Mercurial Mercurial > repos > testboard / 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.
code for while directly, not via while_option
authornipkow
Sun, 04 Nov 2012 18:41:27 +0100
changeset 50008 eb7f574d0303
parent 50007 56f269baae76
child 50009 e48de0410307
code for while directly, not via while_option
src/HOL/Library/While_Combinator.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/While_Combinator.thy	Sun Nov 04 18:38:18 2012 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Sun Nov 04 18:41:27 2012 +0100
@@ -83,7 +83,7 @@
 definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
 where "while b c s = the (while_option b c s)"
 
-lemma while_unfold:
+lemma while_unfold [code]:
   "while b c s = (if b s then while b c (c s) else s)"
 unfolding while_def by (subst while_option_unfold) simp
testboard