1.1 --- a/src/HOL/UNITY/ELT.thy	Tue Feb 21 17:08:32 2012 +0100
     1.2 +++ b/src/HOL/UNITY/ELT.thy	Tue Feb 21 17:09:17 2012 +0100
     1.3 @@ -166,7 +166,7 @@
     1.4  apply (erule leadsETo_induct)
     1.5  prefer 3 apply (blast intro: leadsETo_Union)
     1.6  prefer 2 apply (blast intro: leadsETo_Trans)
     1.7 -apply (blast intro: leadsETo_Basis)
     1.8 +apply blast
     1.9  done
    1.10  
    1.11  lemma leadsETo_Trans_Un:
    1.12 @@ -237,7 +237,7 @@
    1.13  lemma leadsETo_givenBy:
    1.14       "[| F : A leadsTo[CC] A';  CC <= givenBy v |]  
    1.15        ==> F : A leadsTo[givenBy v] A'"
    1.16 -by (blast intro: empty_mem_givenBy leadsETo_weaken)
    1.17 +by (blast intro: leadsETo_weaken)
    1.18  
    1.19  
    1.20  (*Set difference*)
    1.21 @@ -340,7 +340,7 @@
    1.22   apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
    1.23  apply (rule leadsETo_Basis)
    1.24  apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] 
    1.25 -                      Int_Diff ensures_def givenBy_eq_Collect Join_transient)
    1.26 +                      Int_Diff ensures_def givenBy_eq_Collect)
    1.27  prefer 3 apply (blast intro: transient_strengthen)
    1.28  apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
    1.29  apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
    1.30 @@ -454,7 +454,7 @@
    1.31  lemma lel_lemma:
    1.32       "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
    1.33  apply (erule leadsTo_induct)
    1.34 -  apply (blast intro: reachable_ensures leadsETo_Basis)
    1.35 +  apply (blast intro: reachable_ensures)
    1.36   apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
    1.37  apply (subst Int_Union)
    1.38  apply (blast intro: leadsETo_UN)
    1.39 @@ -491,7 +491,7 @@
    1.40        ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]  
    1.41                         (extend_set h B)"
    1.42  apply (erule leadsETo_induct)
    1.43 -  apply (force intro: leadsETo_Basis subset_imp_ensures 
    1.44 +  apply (force intro: subset_imp_ensures 
    1.45                 simp add: extend_ensures extend_set_Diff_distrib [symmetric])
    1.46   apply (blast intro: leadsETo_Trans)
    1.47  apply (simp add: leadsETo_UN extend_set_Union)