Make equivalence_simp work flawlessly with process functions

input-output-hk · Jul 11, 2019 · 9949ea1 · 9949ea1
1 parent 8f0f318
commit 9949ea1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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]
 )