changeset 39754 | 150f831ce4a3 |
parent 32960 | 69916a850301 |
child 41460 | ea56b98aee83 |
--- a/src/HOL/ex/Unification.thy Tue Sep 28 09:43:13 2010 +0200 +++ b/src/HOL/ex/Unification.thy Tue Sep 28 09:54:07 2010 +0200 @@ -158,6 +158,7 @@ Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))" by pat_completeness auto +declare unify.psimps[simp] subsection {* Partial correctness *} @@ -533,4 +534,6 @@ qed qed +declare unify.psimps[simp del] + end