src/HOL/UNITY/Union.thy
changeset 16977 7c04742abac3
parent 16417 9bc16273c2d4
child 30304 d8e4cd2ac2a1
     1.1 --- a/src/HOL/UNITY/Union.thy	Mon Aug 01 19:20:30 2005 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Mon Aug 01 19:20:31 2005 +0200
     1.3 @@ -332,8 +332,10 @@
     1.4  
     1.5  lemma ok_iff_OK:
     1.6       "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
     1.7 -by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
     1.8 -              all_conj_distrib eq_commute,   blast)
     1.9 +apply (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
    1.10 +              all_conj_distrib)
    1.11 +apply blast
    1.12 +done
    1.13  
    1.14  lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)"
    1.15  by (auto simp add: ok_def)