Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
unsymbolize;
authorwenzelm
Thu, 14 Dec 2000 19:37:27 +0100
changeset 10673 337c00fd385b
parent 10672 3b1c2d74a01b
child 10674 2cc6415c1801
unsymbolize;
src/HOL/Library/While_Combinator.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle