1 theory Base |
1 theory Base |
2 imports Main |
2 imports Main |
3 "~~/src/HOL/Library/LaTeXsugar" |
3 "~~/src/HOL/Library/LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
|
6 ML \<open>@{assert} true\<close> |
|
7 ML \<open>@{print} (2 + 3 +4)\<close> |
|
8 |
|
9 |
|
10 print_ML_antiquotations |
|
11 text \<open> |
|
12 Can we put an ML-val into the text? |
|
13 |
|
14 @{ML [display] \<open>2 + 3\<close>} |
|
15 |
|
16 \<close> |
6 notation (latex output) |
17 notation (latex output) |
7 Cons ("_ # _" [66,65] 65) |
18 Cons ("_ # _" [66,65] 65) |
8 |
19 |
9 ML {* |
20 ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
10 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
|
11 |
21 |
12 fun rhs 1 = P 1 |
22 fun rhs 1 = P 1 |
13 | rhs n = HOLogic.mk_conj (P n, rhs (n - 1)) |
23 | rhs n = HOLogic.mk_conj (P n, rhs (n - 1)) |
14 |
24 |
15 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n) |
25 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n) |
16 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
26 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
17 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
27 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
18 |
28 |
19 fun de_bruijn n = |
29 fun de_bruijn n = |
20 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) |
30 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*} |
21 *} |
|
22 |
31 |
23 ML_file "output_tutorial.ML" |
32 ML_file "output_tutorial.ML" |
|
33 text \<open> |
|
34 Can we put an ML-val into the text? |
|
35 |
|
36 @{ML [gray] \<open>2 + 3\<close>} |
|
37 \<close> |
|
38 |
24 ML_file "antiquote_setup.ML" |
39 ML_file "antiquote_setup.ML" |
25 |
40 |
26 setup {* OutputTutorial.setup *} |
41 |
|
42 (*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *) |
27 setup {* AntiquoteSetup.setup *} |
43 setup {* AntiquoteSetup.setup *} |
28 |
44 |
|
45 |
29 end |
46 end |