src/HOL/Library/While_Combinator.thy
changeset 10673 337c00fd385b
parent 10653 55f33da63366
child 10774 4de3a0d3ae28
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Dec 14 19:37:09 2000 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 14 19:37:27 2000 +0100
     1.3 @@ -92,9 +92,9 @@
     1.4  qed
     1.5  
     1.6  theorem while_rule:
     1.7 -  "\<lbrakk> P s; \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> P(c s);
     1.8 -    \<And>s.\<lbrakk> P s; \<not> b s \<rbrakk> \<Longrightarrow> Q s;
     1.9 -    wf r;  \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> (c s,s) \<in> r \<rbrakk> \<Longrightarrow>
    1.10 +  "[| P s; !!s. [| P s; b s  |] ==> P (c s);
    1.11 +    !!s. [| P s; \<not> b s  |] ==> Q s;
    1.12 +    wf r;  !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    1.13      Q (while b c s)"
    1.14  apply (rule while_rule_lemma)
    1.15  prefer 4 apply assumption