src/HOL/UNITY/ProgressSets.thy
changeset 56166 9a241bc276cd
parent 51488 3c886fe611b8
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Sat Mar 15 16:54:32 2014 +0100
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Sun Mar 16 18:09:04 2014 +0100
     1.3 @@ -257,7 +257,7 @@
     1.4   apply (simp add: progress_induction_step) 
     1.5  txt{*Disjunctive case*}
     1.6  apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
     1.7 - apply (simp add: Int_Union) 
     1.8 + apply simp 
     1.9  apply (blast intro: UN_in_lattice) 
    1.10  done
    1.11