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 print_ML_antiquotations |
|
7 |
|
8 text \<open> |
|
9 Why is Base not printed? |
|
10 @{cite "isa-imp"} |
|
11 \<close> |
|
12 notation (latex output) |
6 notation (latex output) |
13 Cons ("_ # _" [66,65] 65) |
7 Cons ("_ # _" [66,65] 65) |
14 |
8 |
15 ML %linenosgrayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
9 ML %linenosgrayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
16 |
10 |
25 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))\<close> |
19 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))\<close> |
26 |
20 |
27 ML_file "output_tutorial.ML" |
21 ML_file "output_tutorial.ML" |
28 ML_file "antiquote_setup.ML" |
22 ML_file "antiquote_setup.ML" |
29 |
23 |
30 |
|
31 (*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *) |
|
32 setup \<open>AntiquoteSetup.setup\<close> |
24 setup \<open>AntiquoteSetup.setup\<close> |
33 |
25 |
34 print_ML_antiquotations |
|
35 |
|
36 end |
26 end |