23
|
1 |
theory Base
|
459
|
2 |
imports Main
|
|
3 |
"~~/src/HOL/Library/LaTeXsugar"
|
23
|
4 |
begin
|
|
5 |
|
564
|
6 |
print_ML_antiquotations
|
562
|
7 |
|
564
|
8 |
text \<open>Hallo ML Antiquotation:
|
|
9 |
@{ML \<open>2 + 3\<close>}
|
|
10 |
\<close>
|
562
|
11 |
|
394
|
12 |
notation (latex output)
|
|
13 |
Cons ("_ # _" [66,65] 65)
|
|
14 |
|
562
|
15 |
ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
|
396
|
16 |
|
|
17 |
fun rhs 1 = P 1
|
|
18 |
| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
|
|
19 |
|
|
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
|
|
22 |
(HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
|
|
23 |
|
|
24 |
fun de_bruijn n =
|
562
|
25 |
HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
|
346
|
26 |
|
538
|
27 |
ML_file "output_tutorial.ML"
|
|
28 |
ML_file "antiquote_setup.ML"
|
346
|
29 |
|
562
|
30 |
|
|
31 |
(*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)
|
471
|
32 |
setup {* AntiquoteSetup.setup *}
|
346
|
33 |
|
564
|
34 |
print_ML_antiquotations
|
|
35 |
|
|
36 |
text \<open>Hallo ML Antiquotation:
|
|
37 |
@{ML \<open>2 + 3\<close> }
|
|
38 |
\<close>
|
562
|
39 |
|
239
|
40 |
end |