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
--- 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