src/HOL/UNITY/ProgressSets.thy
changeset 32693 6c6b1ba5e71e
parent 32604 8b3e2bc91a46
child 32960 69916a850301
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Sep 21 15:35:14 2009 +0200
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Sep 21 15:35:15 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/UNITY/ProgressSets
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   2003  University of Cambridge
     1.8  
     1.9 @@ -245,7 +244,7 @@
    1.10    then have "cl C (T\<inter>?r) \<subseteq> ?r"
    1.11      by (blast intro!: subset_wens) 
    1.12    then have cl_subset: "cl C (T\<inter>?r) \<subseteq> T\<inter>?r"
    1.13 -    by (simp add: Int_subset_iff cl_ident TC
    1.14 +    by (simp add: cl_ident TC
    1.15                    subset_trans [OF cl_mono [OF Int_lower1]]) 
    1.16    show ?thesis
    1.17      by (rule cl_subset_in_lattice [OF cl_subset latt]) 
    1.18 @@ -486,7 +485,7 @@
    1.19    shows "closed F T B L"
    1.20  apply (simp add: closed_def, clarify)
    1.21  apply (rule ProgressSets.cl_subset_in_lattice [OF _ lattice])  
    1.22 -apply (simp add: Int_Un_distrib cl_Un [OF lattice] Un_subset_iff 
    1.23 +apply (simp add: Int_Un_distrib cl_Un [OF lattice] 
    1.24                   cl_ident Int_in_lattice [OF TL BL lattice] Un_upper1)
    1.25  apply (subgoal_tac "cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T \<inter> M)))") 
    1.26   prefer 2