src/HOL/UNITY/Guar.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 13819 78f5885b76a9
     1.1 --- a/src/HOL/UNITY/Guar.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Guar.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -109,8 +109,7 @@
     1.4  lemma ex_prop_equiv: 
     1.5       "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
     1.6  apply auto
     1.7 -apply (unfold ex_prop_def component_of_def, safe)
     1.8 -apply blast 
     1.9 +apply (unfold ex_prop_def component_of_def, safe, blast) 
    1.10  apply blast 
    1.11  apply (subst Join_commute) 
    1.12  apply (drule ok_sym, blast)