src/HOL/Library/Multiset.thy
changeset 11549 e7265e70fd7c
parent 11464 ddea204de5bc
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Sep 04 17:31:18 2001 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Sep 04 21:10:57 2001 +0200
     1.3 @@ -331,8 +331,8 @@
     1.4    "P (\<lambda>a. 0) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1')))
     1.5      ==> \<forall>f. f \<in> multiset --> setsum f {x. 0 < f x} = n --> P f"
     1.6  proof -
     1.7 -  case antecedent
     1.8 -  note prems = this [unfolded multiset_def]
     1.9 +  case rule_context
    1.10 +  note premises = this [unfolded multiset_def]
    1.11    show ?thesis
    1.12      apply (unfold multiset_def)
    1.13      apply (induct_tac n)
    1.14 @@ -340,7 +340,7 @@
    1.15       apply clarify
    1.16       apply (subgoal_tac "f = (\<lambda>a.0)")
    1.17        apply simp
    1.18 -      apply (rule prems)
    1.19 +      apply (rule premises)
    1.20       apply (rule ext)
    1.21       apply force
    1.22      apply clarify
    1.23 @@ -358,7 +358,7 @@
    1.24       prefer 2
    1.25       apply (rule ext)
    1.26       apply (simp (no_asm_simp))
    1.27 -     apply (erule ssubst, rule prems)
    1.28 +     apply (erule ssubst, rule premises)
    1.29       apply blast
    1.30      apply (erule allE, erule impE, erule_tac [2] mp)
    1.31       apply blast