equal
deleted
inserted
replaced
3 "~~/src/HOL/Library/LaTeXsugar" |
3 "~~/src/HOL/Library/LaTeXsugar" |
4 (*keywords "ML" "setup" "local_setup" :: thy_decl and |
4 (*keywords "ML" "setup" "local_setup" :: thy_decl and |
5 "ML_prf" :: prf_decl and |
5 "ML_prf" :: prf_decl and |
6 "ML_val" :: diag |
6 "ML_val" :: diag |
7 *) |
7 *) |
8 uses |
|
9 ("output_tutorial.ML") |
|
10 ("antiquote_setup.ML") |
|
11 begin |
8 begin |
12 |
9 |
13 notation (latex output) |
10 notation (latex output) |
14 Cons ("_ # _" [66,65] 65) |
11 Cons ("_ # _" [66,65] 65) |
15 |
12 |
25 |
22 |
26 fun de_bruijn n = |
23 fun de_bruijn n = |
27 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) |
24 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) |
28 *} |
25 *} |
29 |
26 |
30 use "output_tutorial.ML" |
27 ML_file "output_tutorial.ML" |
31 use "antiquote_setup.ML" |
28 ML_file "antiquote_setup.ML" |
32 |
29 |
33 setup {* OutputTutorial.setup *} |
30 setup {* OutputTutorial.setup *} |
34 setup {* AntiquoteSetup.setup *} |
31 setup {* AntiquoteSetup.setup *} |
35 |
32 |
36 end |
33 end |