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