src/HOL/UNITY/Transformers.thy
changeset 15236 f289e8ba2bb3
parent 15102 04b0e943fcc9
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Oct 11 07:39:19 2004 +0200
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Oct 11 07:42:22 2004 +0200
     1.3 @@ -403,21 +403,21 @@
     1.4  
     1.5  lemma wens_single_finite_subset_wens_single:
     1.6        "wens_single_finite act B k \<subseteq> wens_single act B"
     1.7 -by (simp add: wens_single_eq_Union, blast) 
     1.8 +by (simp add: wens_single_eq_Union, blast)
     1.9  
    1.10  lemma subset_wens_single_finite:
    1.11        "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
    1.12         ==> \<exists>m. \<Union>W = wens_single_finite act B m"
    1.13  apply (induct k)
    1.14 - apply (rule_tac x=0 in exI, simp, blast) 
    1.15 -apply (auto simp add: atMost_Suc) 
    1.16 -apply (case_tac "wens_single_finite act B (Suc n) \<in> W") 
    1.17 - prefer 2 apply blast 
    1.18 -apply (drule_tac x="Suc n" in spec)
    1.19 + apply (rule_tac x=0 in exI, simp, blast)
    1.20 +apply (auto simp add: atMost_Suc)
    1.21 +apply (case_tac "wens_single_finite act B (Suc k) \<in> W")
    1.22 + prefer 2 apply blast
    1.23 +apply (drule_tac x="Suc k" in spec)
    1.24  apply (erule notE, rule equalityI)
    1.25 - prefer 2 apply blast 
    1.26 -apply (subst wens_single_finite_eq_Union) 
    1.27 -apply (simp add: atMost_Suc, blast) 
    1.28 + prefer 2 apply blast
    1.29 +apply (subst wens_single_finite_eq_Union)
    1.30 +apply (simp add: atMost_Suc, blast)
    1.31  done
    1.32  
    1.33  text{*lemma for Union case*}