changeset 44870 | 0d23a8ae14df |
parent 35416 | d8d7d1b785af |
child 45605 | a89b4bc311a5 |
--- a/src/HOL/UNITY/Constrains.thy Sat Sep 10 20:41:27 2011 +0200 +++ b/src/HOL/UNITY/Constrains.thy Sat Sep 10 21:47:55 2011 +0200 @@ -181,7 +181,9 @@ lemma Constrains_cancel: "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')" -by (simp add: Constrains_eq_constrains constrains_def, blast) +apply (simp add: Constrains_eq_constrains constrains_def) +apply best +done subsection{*Stable*}