diff -r 021cf00435a9 -r a9bb54a3cfb7 src/HOL/Main.thy --- a/src/HOL/Main.thy Mon Dec 16 11:18:35 2002 +0100 +++ b/src/HOL/Main.thy Mon Dec 16 13:43:11 2002 +0100 @@ -39,7 +39,12 @@ "wfrec" ("wf'_rec?") -ML {* fun wf_rec f x = f (wf_rec f) x; *} +ML {* +fun wf_rec f x = f (wf_rec f) x; + +val term_of_list = HOLogic.mk_list; +val term_of_int = HOLogic.mk_int; +*} lemma [code]: "((n::nat) < 0) = False" by simp declare less_Suc_eq [code]