src/HOL/UNITY/Follows.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 15102 04b0e943fcc9
     1.1 --- a/src/HOL/UNITY/Follows.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Follows.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -62,16 +62,13 @@
     1.4  subsection{*Destruction rules*}
     1.5  
     1.6  lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
     1.7 -apply (unfold Follows_def, blast)
     1.8 -done
     1.9 +by (unfold Follows_def, blast)
    1.10  
    1.11  lemma Follows_Increasing2: "F \<in> f Fols g ==> F \<in> Increasing g"
    1.12 -apply (unfold Follows_def, blast)
    1.13 -done
    1.14 +by (unfold Follows_def, blast)
    1.15  
    1.16  lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<subseteq> g s}"
    1.17 -apply (unfold Follows_def, blast)
    1.18 -done
    1.19 +by (unfold Follows_def, blast)
    1.20  
    1.21  lemma Follows_LeadsTo: 
    1.22       "F \<in> f Fols g ==> F \<in> {s. k \<le> g s} LeadsTo {s. k \<le> f s}"
    1.23 @@ -159,8 +156,7 @@
    1.24  apply (rule LeadsTo_weaken)
    1.25  apply (rule PSP_Stable)
    1.26  apply (erule_tac x = "f s" in spec)
    1.27 -apply (erule Stable_Int, assumption)
    1.28 -apply blast+
    1.29 +apply (erule Stable_Int, assumption, blast+)
    1.30  done
    1.31  
    1.32  lemma Follows_Un: 
    1.33 @@ -218,8 +214,7 @@
    1.34  apply (rule LeadsTo_weaken)
    1.35  apply (rule PSP_Stable)
    1.36  apply (erule_tac x = "f s" in spec)
    1.37 -apply (erule Stable_Int, assumption)
    1.38 -apply blast
    1.39 +apply (erule Stable_Int, assumption, blast)
    1.40  apply (blast intro: union_le_mono order_trans)
    1.41  done
    1.42