# HG changeset patch
# User wenzelm
# Date 976819047 -3600
# Node ID 337c00fd385b465d9cc75b163c5e9fd787a4b0e6
# Parent  3b1c2d74a01be166dffa060da1d957f7de7665ca
unsymbolize;

diff -r 3b1c2d74a01b -r 337c00fd385b src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Thu Dec 14 19:37:09 2000 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Thu Dec 14 19:37:27 2000 +0100
@@ -92,9 +92,9 @@
 qed
 
 theorem while_rule:
-  "\<lbrakk> P s; \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> P(c s);
-    \<And>s.\<lbrakk> P s; \<not> b s \<rbrakk> \<Longrightarrow> Q s;
-    wf r;  \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> (c s,s) \<in> r \<rbrakk> \<Longrightarrow>
+  "[| P s; !!s. [| P s; b s  |] ==> P (c s);
+    !!s. [| P s; \<not> b s  |] ==> Q s;
+    wf r;  !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
     Q (while b c s)"
 apply (rule while_rule_lemma)
 prefer 4 apply assumption