# HG changeset patch
# User kleing
# Date 1011276396 -3600
# Node ID ccc0f45ad2c438430377fe3ab020206e3326eb9c
# Parent  8108791e29060bb64817180bd5b55863874d5594
registered directly executable version with the code generator

diff -r 8108791e2906 -r ccc0f45ad2c4 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Thu Jan 17 12:58:31 2002 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Thu Jan 17 15:06:36 2002 +0100
@@ -54,7 +54,7 @@
  The recursion equation for @{term while}: directly executable!
 *}
 
-theorem while_unfold:
+theorem while_unfold [code]:
     "while b c s = (if b s then while b c (c s) else s)"
   apply (unfold while_def)
   apply (rule while_aux_unfold [THEN trans])