src/HOL/UNITY/ProgressSets.thy
changeset 15102 04b0e943fcc9
parent 14150 9a23e4eb5eb3
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Aug 02 16:06:13 2004 +0200
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Tue Aug 03 13:48:00 2004 +0200
     1.3 @@ -486,11 +486,11 @@
     1.4    shows "closed F T B L"
     1.5  apply (simp add: closed_def, clarify)
     1.6  apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
     1.7 -apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff
     1.8 +apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff 
     1.9                   cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
    1.10  apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
    1.11   prefer 2 
    1.12 - apply (simp add: commutes [unfolded commutes_def]) 
    1.13 + apply (cut_tac commutes, simp add: commutes_def) 
    1.14  apply (erule subset_trans) 
    1.15  apply (simp add: cl_ident)
    1.16  apply (blast intro: rev_subsetD [OF _ wp_mono]) 
    1.17 @@ -548,7 +548,7 @@
    1.18        and TL: "T \<in> L"
    1.19        and Fstable: "F \<in> stable T"
    1.20    shows  "commutes F T B L"
    1.21 -apply (simp add: commutes_def, clarify)  
    1.22 +apply (simp add: commutes_def del: Int_subset_iff, clarify)  
    1.23  apply (rename_tac t)
    1.24  apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") 
    1.25   prefer 2