equal
deleted
inserted
replaced
3 "~~/src/HOL/Library/LaTeXsugar" |
3 "~~/src/HOL/Library/LaTeXsugar" |
4 begin |
4 begin |
5 |
5 |
6 print_ML_antiquotations |
6 print_ML_antiquotations |
7 |
7 |
8 text \<open>Hallo ML Antiquotation: |
8 text \<open> |
9 @{ML \<open>2 + 3\<close>} |
9 Why is Base not printed? |
|
10 @{cite "isa-imp"} |
10 \<close> |
11 \<close> |
11 |
|
12 notation (latex output) |
12 notation (latex output) |
13 Cons ("_ # _" [66,65] 65) |
13 Cons ("_ # _" [66,65] 65) |
14 |
14 |
15 ML %linenosgrayML\<open>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 |
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 \<open>AntiquoteSetup.setup\<close> |
32 setup \<open>AntiquoteSetup.setup\<close> |
33 |
33 |
34 print_ML_antiquotations |
34 print_ML_antiquotations |
35 |
35 |
36 text \<open>Hallo ML Antiquotation: |
|
37 @{ML \<open>2 + 3\<close> } |
|
38 \<close> |
|
39 |
|
40 end |
36 end |