# HG changeset patch
# User nipkow
# Date 1352050887 -3600
# Node ID eb7f574d03032af996526a6871bfb753f2bab48b
# Parent  56f269baae7676816df3d71243143d5661cfa5e3
code for while directly, not via while_option

diff -r 56f269baae76 -r eb7f574d0303 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