equal
deleted
inserted
replaced
286 "wfrec" ("\<module>wfrec?") |
286 "wfrec" ("\<module>wfrec?") |
287 attach {* |
287 attach {* |
288 fun wfrec f x = f (wfrec f) x; |
288 fun wfrec f x = f (wfrec f) x; |
289 *} |
289 *} |
290 |
290 |
|
291 code_primconst wfrec |
|
292 ml {* |
|
293 fun wfrec f x = f (wfrec f) x; |
|
294 *} |
|
295 haskell {* |
|
296 wfrec f x = f (wfrec f) x |
|
297 *} |
|
298 |
|
299 (* code_syntax_const |
|
300 wfrec |
|
301 ml ("{*wfrec*}?") |
|
302 haskell ("{*wfrec*}?") *) |
291 |
303 |
292 subsection{*Variants for TFL: the Recdef Package*} |
304 subsection{*Variants for TFL: the Recdef Package*} |
293 |
305 |
294 lemma tfl_wf_induct: "ALL R. wf R --> |
306 lemma tfl_wf_induct: "ALL R. wf R --> |
295 (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" |
307 (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" |