Skip to content
Permalink
Browse files

Make `equivalence_simp` work flawlessly with process functions

  • Loading branch information...
jeltsch committed Jul 11, 2019
1 parent 8f0f318 commit 9949ea1d2dace0391c257addb160515748641349
Showing with 1 addition and 1 deletion.
  1. +1 −1 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]
)

0 comments on commit 9949ea1

Please sign in to comment.
You can’t perform that action at this time.