src/HOL/UNITY/ProgressSets.thy
changeset 59807 22bc39064290
parent 58889 5b7a9633cfa8
child 62343 24106dc44def
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Wed Mar 25 10:41:53 2015 +0100
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Wed Mar 25 10:44:57 2015 +0100
     1.3 @@ -383,7 +383,7 @@
     1.4  apply (drule equalityD1)   
     1.5  apply (rule subset_trans) 
     1.6   prefer 2 apply assumption
     1.7 -apply (thin_tac "?U \<subseteq> X") 
     1.8 +apply (thin_tac "_ \<subseteq> X") 
     1.9  apply (cut_tac A=X in UN_singleton) 
    1.10  apply (erule subst) 
    1.11  apply (simp only: cl_UN lattice_latticeof