# HG changeset patch
# User berghofe
# Date 1019220693 -7200
# Node ID ab033530790541677e622fb4f134b9f0fb57f0b2
# Parent  eae72c47d07fd7fe5f9e8b1f5efb3b8d3d21f968
code generator: wfrec combinator is now implemented by ML function wf_rec.

diff -r eae72c47d07f -r ab0335307905 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Apr 19 14:47:10 2002 +0200
+++ b/src/HOL/Main.thy	Fri Apr 19 14:51:33 2002 +0200
@@ -116,6 +116,10 @@
   "Nil"     ("[]")
   "Cons"    ("(_ ::/ _)")
 
+  "wfrec"   ("wf'_rec?")
+
+ML {* fun wf_rec f x = f (wf_rec f) x; *}
+
 lemma [code]: "((n::nat) < 0) = False" by simp
 declare less_Suc_eq [code]