18 numeral :: num \<Rightarrow> nat, Num.One, Num.Bit0, Num.Bit1, |
18 numeral :: num \<Rightarrow> nat, Num.One, Num.Bit0, Num.Bit1, |
19 Code_Evaluation.TERM_OF_EQUAL :: int list itself)" |
19 Code_Evaluation.TERM_OF_EQUAL :: int list itself)" |
20 |
20 |
21 ML \<open> |
21 ML \<open> |
22 local |
22 local |
23 val ctxt = @{context}; |
23 val ctxt = \<^context>; |
24 val consts = [@{const_name required_symbols}]; |
24 val consts = [\<^const_name>\<open>required_symbols\<close>]; |
25 in |
25 in |
26 val simp = Code_Simp.static_conv |
26 val simp = Code_Simp.static_conv |
27 { ctxt = ctxt, consts = consts, simpset = NONE }; |
27 { ctxt = ctxt, consts = consts, simpset = NONE }; |
28 val nbe = Nbe.static_conv |
28 val nbe = Nbe.static_conv |
29 { ctxt = ctxt, consts = consts }; |
29 { ctxt = ctxt, consts = consts }; |
30 end; |
30 end; |
31 \<close> |
31 \<close> |
32 |
32 |
33 ML_val \<open> |
33 ML_val \<open> |
34 simp @{context} @{cterm "primes_upto 100"} |
34 simp \<^context> \<^cterm>\<open>primes_upto 100\<close> |
35 \<close> |
35 \<close> |
36 |
36 |
37 ML_val \<open> |
37 ML_val \<open> |
38 simp @{context} @{cterm "primes_upto 200"} |
38 simp \<^context> \<^cterm>\<open>primes_upto 200\<close> |
39 \<close> |
39 \<close> |
40 |
40 |
41 ML_val \<open> |
41 ML_val \<open> |
42 nbe @{context} @{cterm "primes_upto 200"} |
42 nbe \<^context> \<^cterm>\<open>primes_upto 200\<close> |
43 \<close> |
43 \<close> |
44 |
44 |
45 ML_val \<open> |
45 ML_val \<open> |
46 nbe @{context} @{cterm "primes_upto 400"} |
46 nbe \<^context> \<^cterm>\<open>primes_upto 400\<close> |
47 \<close> |
47 \<close> |
48 |
48 |
49 ML_val \<open> |
49 ML_val \<open> |
50 nbe @{context} @{cterm "primes_upto 600"} |
50 nbe \<^context> \<^cterm>\<open>primes_upto 600\<close> |
51 \<close> |
51 \<close> |
52 |
52 |
53 end |
53 end |