unsymbolize;
authorwenzelm
Thu Dec 14 19:37:27 2000 +0100 (2000-12-14)
changeset 10673337c00fd385b
parent 10672 3b1c2d74a01b
child 10674 2cc6415c1801
unsymbolize;
src/HOL/Library/While_Combinator.thy
     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