Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/While_Combinator.thy
changeset 67717 5a1b299fe4af
parent 67613 ce654b0e6d69
child 69593 3dda49e08b9d 
--- a/src/HOL/Library/While_Combinator.thy	Fri Feb 23 21:46:30 2018 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Sat Feb 24 17:21:35 2018 +0100
@@ -68,7 +68,7 @@
   define k where "k = (LEAST k. \<not> b ((c ^^ k) s))"
   from assms have t: "t = (c ^^ k) s"
     by (simp add: while_option_def k_def split: if_splits)    
-  have 1: "ALL i<k. b ((c ^^ i) s)"
+  have 1: "\<forall>i<k. b ((c ^^ i) s)"
     by (auto simp: k_def dest: not_less_Least)
 
   { fix i assume "i \<le> k" then have "P ((c ^^ i) s)"
isabelle