equal
deleted
inserted
replaced
295 CodegenPackage.add_appconst ("wfrec", CodegenPackage.appgen_wfrec) |
295 CodegenPackage.add_appconst ("wfrec", CodegenPackage.appgen_wfrec) |
296 *} |
296 *} |
297 |
297 |
298 code_constapp |
298 code_constapp |
299 wfrec |
299 wfrec |
300 ml ("let fun wfrec f x = f (wfrec f) x in wfrec _ _ end;") |
300 ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)") |
301 haskell ("wfrec _ _ where wfrec f x = f (wfrec f) x") |
301 haskell (target_atom "(wfrec where wfrec f x = f (wfrec f) x)") |
302 |
302 |
303 subsection{*Variants for TFL: the Recdef Package*} |
303 subsection{*Variants for TFL: the Recdef Package*} |
304 |
304 |
305 lemma tfl_wf_induct: "ALL R. wf R --> |
305 lemma tfl_wf_induct: "ALL R. wf R --> |
306 (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" |
306 (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))" |