1.1 --- a/src/HOL/UNITY/Union.thy	Tue Feb 21 17:08:32 2012 +0100
     1.2 +++ b/src/HOL/UNITY/Union.thy	Tue Feb 21 17:09:17 2012 +0100
     1.3 @@ -202,7 +202,7 @@
     1.4  
     1.5  lemma Join_unless [simp]:
     1.6       "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
     1.7 -by (simp add: Join_constrains unless_def)
     1.8 +by (simp add: unless_def)
     1.9  
    1.10  (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
    1.11    reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
    1.12 @@ -238,12 +238,12 @@
    1.13  lemma Join_increasing [simp]:
    1.14       "(F\<squnion>G \<in> increasing f) =  
    1.15        (F \<in> increasing f & G \<in> increasing f)"
    1.16 -by (simp add: increasing_def Join_stable, blast)
    1.17 +by (auto simp add: increasing_def)
    1.18  
    1.19  lemma invariant_JoinI:
    1.20       "[| F \<in> invariant A; G \<in> invariant A |]   
    1.21        ==> F\<squnion>G \<in> invariant A"
    1.22 -by (simp add: invariant_def, blast)
    1.23 +by (auto simp add: invariant_def)
    1.24  
    1.25  lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
    1.26  by (simp add: FP_def JN_stable INTER_eq)
    1.27 @@ -262,10 +262,10 @@
    1.28  by (auto simp add: bex_Un transient_def Join_def)
    1.29  
    1.30  lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
    1.31 -by (simp add: Join_transient)
    1.32 +by simp
    1.33  
    1.34  lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
    1.35 -by (simp add: Join_transient)
    1.36 +by simp
    1.37  
    1.38  (*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
    1.39  lemma JN_ensures:
    1.40 @@ -278,7 +278,7 @@
    1.41       "F\<squnion>G \<in> A ensures B =      
    1.42        (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &  
    1.43         (F \<in> transient (A-B) | G \<in> transient (A-B)))"
    1.44 -by (auto simp add: ensures_def Join_transient)
    1.45 +by (auto simp add: ensures_def)
    1.46  
    1.47  lemma stable_Join_constrains: 
    1.48      "[| F \<in> stable A;  G \<in> A co A' |]