Merge pull request #95 from input-output-hk/bug/equivalence-simp-with…

…-process-functions Make `equivalence_simp` work flawlessly with process functions
input-output-hk · Jul 11, 2019 · 30b3620 · 30b3620
2 parents 8f0f318 + 9949ea1
commit 30b3620
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]
 )