code for while directly, not via while_option
authornipkow
Sun Nov 04 18:41:27 2012 +0100 (2012-11-04)
changeset 50008eb7f574d0303
parent 50007 56f269baae76
child 50009 e48de0410307
code for while directly, not via while_option
src/HOL/Library/While_Combinator.thy
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Sun Nov 04 18:38:18 2012 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Sun Nov 04 18:41:27 2012 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  definition while :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
     1.5  where "while b c s = the (while_option b c s)"
     1.6  
     1.7 -lemma while_unfold:
     1.8 +lemma while_unfold [code]:
     1.9    "while b c s = (if b s then while b c (c s) else s)"
    1.10  unfolding while_def by (subst while_option_unfold) simp
    1.11