1.1 --- a/src/HOL/Library/While_Combinator.thy	Thu Jan 17 12:58:31 2002 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Thu Jan 17 15:06:36 2002 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4   The recursion equation for @{term while}: directly executable!
     1.5  *}
     1.6  
     1.7 -theorem while_unfold:
     1.8 +theorem while_unfold [code]:
     1.9      "while b c s = (if b s then while b c (c s) else s)"
    1.10    apply (unfold while_def)
    1.11    apply (rule while_aux_unfold [THEN trans])