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.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
```