equal
deleted
inserted
replaced
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> |
6 print_ML_antiquotations |
7 ML \<open>@{print} (2 + 3 +4)\<close> |
|
8 |
7 |
|
8 text \<open>Hallo ML Antiquotation: |
|
9 @{ML \<open>2 + 3\<close>} |
|
10 \<close> |
9 |
11 |
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> |
|
17 notation (latex output) |
12 notation (latex output) |
18 Cons ("_ # _" [66,65] 65) |
13 Cons ("_ # _" [66,65] 65) |
19 |
14 |
20 ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
15 ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
21 |
16 |
28 |
23 |
29 fun de_bruijn n = |
24 fun de_bruijn n = |
30 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*} |
25 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*} |
31 |
26 |
32 ML_file "output_tutorial.ML" |
27 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 |
|
39 ML_file "antiquote_setup.ML" |
28 ML_file "antiquote_setup.ML" |
40 |
29 |
41 |
30 |
42 (*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 *) |
43 setup {* AntiquoteSetup.setup *} |
32 setup {* AntiquoteSetup.setup *} |
44 |
33 |
|
34 print_ML_antiquotations |
|
35 |
|
36 text \<open>Hallo ML Antiquotation: |
|
37 @{ML \<open>2 + 3\<close> } |
|
38 \<close> |
45 |
39 |
46 end |
40 end |