speed up slow proof;
authorwenzelm
Sat Sep 10 21:47:55 2011 +0200 (2011-09-10)
changeset 448700d23a8ae14df
parent 44869 328825888426
child 44871 fbfdc5ac86be
child 44873 045fedcfadf6
speed up slow proof;
src/HOL/UNITY/Constrains.thy
     1.1 --- a/src/HOL/UNITY/Constrains.thy	Sat Sep 10 20:41:27 2011 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.thy	Sat Sep 10 21:47:55 2011 +0200
     1.3 @@ -181,7 +181,9 @@
     1.4  
     1.5  lemma Constrains_cancel:
     1.6       "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
     1.7 -by (simp add: Constrains_eq_constrains constrains_def, blast)
     1.8 +apply (simp add: Constrains_eq_constrains constrains_def)
     1.9 +apply best
    1.10 +done
    1.11  
    1.12  
    1.13  subsection{*Stable*}