From 9949ea1d2dace0391c257addb160515748641349 Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Fri, 12 Jul 2019 00:12:16 +0300 Subject: [PATCH] Make `equivalence_simp` work flawlessly with process functions --- Isabelle/Utilities/Equivalences.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Isabelle/Utilities/Equivalences.thy b/Isabelle/Utilities/Equivalences.thy index 884519e..4134627 100644 --- a/Isabelle/Utilities/Equivalences.thy +++ b/Isabelle/Utilities/Equivalences.thy @@ -5,7 +5,7 @@ begin named_theorems equivalence_simp_goal_preparation and equivalence_simp method equivalence_simp = ( - simp only: equivalence_simp_goal_preparation [THEN sym]; + simp only: equivalence_simp_goal_preparation [THEN sym] id_def comp_def; simp only: equivalence_simp [transferred] )