src/HOL/Library/While_Combinator.thy
changeset 11549 e7265e70fd7c
parent 11284 981ea92a86dd
child 11626 0dbfb578bf75
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Sep 04 17:31:18 2001 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Sep 04 21:10:57 2001 +0200
     1.3 @@ -79,14 +79,14 @@
     1.4        wf {(t, s). P s \<and> b s \<and> t = c s} |] ==>
     1.5      P s --> Q (while b c s)"
     1.6  proof -
     1.7 -  case antecedent
     1.8 +  case rule_context
     1.9    assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"
    1.10    show ?thesis
    1.11      apply (induct s rule: wf [THEN wf_induct])
    1.12      apply simp
    1.13      apply clarify
    1.14      apply (subst while_unfold)
    1.15 -    apply (simp add: antecedent)
    1.16 +    apply (simp add: rule_context)
    1.17      done
    1.18  qed
    1.19