src/HOL/Main.thy
changeset 13755 a9bb54a3cfb7
parent 13403 bc2b32ee62fd
child 14049 ef1da11a64b9
     1.1 --- a/src/HOL/Main.thy	Mon Dec 16 11:18:35 2002 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Dec 16 13:43:11 2002 +0100
     1.3 @@ -39,7 +39,12 @@
     1.4  
     1.5    "wfrec"   ("wf'_rec?")
     1.6  
     1.7 -ML {* fun wf_rec f x = f (wf_rec f) x; *}
     1.8 +ML {*
     1.9 +fun wf_rec f x = f (wf_rec f) x;
    1.10 +
    1.11 +val term_of_list = HOLogic.mk_list;
    1.12 +val term_of_int = HOLogic.mk_int;
    1.13 +*}
    1.14  
    1.15  lemma [code]: "((n::nat) < 0) = False" by simp
    1.16  declare less_Suc_eq [code]