changeset 13093 | ab0335307905 |
parent 12554 | 671b4d632c34 |
child 13367 | ad307f0d80db |
--- 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]