equal
deleted
inserted
replaced
37 "Nil" ("[]") |
37 "Nil" ("[]") |
38 "Cons" ("(_ ::/ _)") |
38 "Cons" ("(_ ::/ _)") |
39 |
39 |
40 "wfrec" ("wf'_rec?") |
40 "wfrec" ("wf'_rec?") |
41 |
41 |
42 ML {* fun wf_rec f x = f (wf_rec f) x; *} |
42 ML {* |
|
43 fun wf_rec f x = f (wf_rec f) x; |
|
44 |
|
45 val term_of_list = HOLogic.mk_list; |
|
46 val term_of_int = HOLogic.mk_int; |
|
47 *} |
43 |
48 |
44 lemma [code]: "((n::nat) < 0) = False" by simp |
49 lemma [code]: "((n::nat) < 0) = False" by simp |
45 declare less_Suc_eq [code] |
50 declare less_Suc_eq [code] |
46 |
51 |
47 end |
52 end |