10 \<close> |
10 \<close> |
11 |
11 |
12 notation (latex output) |
12 notation (latex output) |
13 Cons ("_ # _" [66,65] 65) |
13 Cons ("_ # _" [66,65] 65) |
14 |
14 |
15 ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
15 ML %linenosgrayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
16 |
16 |
17 fun rhs 1 = P 1 |
17 fun rhs 1 = P 1 |
18 | rhs n = HOLogic.mk_conj (P n, rhs (n - 1)) |
18 | rhs n = HOLogic.mk_conj (P n, rhs (n - 1)) |
19 |
19 |
20 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n) |
20 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n) |
21 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
21 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
22 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
22 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
23 |
23 |
24 fun de_bruijn n = |
24 fun de_bruijn n = |
25 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*} |
25 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))\<close> |
26 |
26 |
27 ML_file "output_tutorial.ML" |
27 ML_file "output_tutorial.ML" |
28 ML_file "antiquote_setup.ML" |
28 ML_file "antiquote_setup.ML" |
29 |
29 |
30 |
30 |
31 (*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *) |
31 (*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *) |
32 setup {* AntiquoteSetup.setup *} |
32 setup \<open>AntiquoteSetup.setup\<close> |
33 |
33 |
34 print_ML_antiquotations |
34 print_ML_antiquotations |
35 |
35 |
36 text \<open>Hallo ML Antiquotation: |
36 text \<open>Hallo ML Antiquotation: |
37 @{ML \<open>2 + 3\<close> } |
37 @{ML \<open>2 + 3\<close> } |