equal
deleted
inserted
replaced
52 |
52 |
53 text {* |
53 text {* |
54 The recursion equation for @{term while}: directly executable! |
54 The recursion equation for @{term while}: directly executable! |
55 *} |
55 *} |
56 |
56 |
57 theorem while_unfold: |
57 theorem while_unfold [code]: |
58 "while b c s = (if b s then while b c (c s) else s)" |
58 "while b c s = (if b s then while b c (c s) else s)" |
59 apply (unfold while_def) |
59 apply (unfold while_def) |
60 apply (rule while_aux_unfold [THEN trans]) |
60 apply (rule while_aux_unfold [THEN trans]) |
61 apply auto |
61 apply auto |
62 apply (subst while_aux_unfold) |
62 apply (subst while_aux_unfold) |