changeset 12791 | ccc0f45ad2c4 |
parent 11914 | bca734def300 |
child 14300 | bf8b8c9425c3 |
--- 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])