equal
deleted
inserted
replaced
5 ("antiquote_setup.ML") |
5 ("antiquote_setup.ML") |
6 begin |
6 begin |
7 |
7 |
8 notation (latex output) |
8 notation (latex output) |
9 Cons ("_ # _" [66,65] 65) |
9 Cons ("_ # _" [66,65] 65) |
10 |
|
11 |
10 |
12 (* rebinding of writeln and tracing so that it can *) |
11 (* rebinding of writeln and tracing so that it can *) |
13 (* be compared in intiquotations *) |
12 (* be compared in intiquotations *) |
14 ML {* |
13 ML {* |
15 fun writeln s = (Output.writeln s; s) |
14 fun writeln s = (Output.writeln s; s) |
139 (OuterKeyword.tag_ml OuterKeyword.thy_decl) |
138 (OuterKeyword.tag_ml OuterKeyword.thy_decl) |
140 (OuterParse.ML_source >> (fn (txt, pos) => |
139 (OuterParse.ML_source >> (fn (txt, pos) => |
141 IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
140 IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
142 *} |
141 *} |
143 |
142 |
|
143 ML {* |
|
144 fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) |
|
145 |
|
146 fun rhs 1 = P 1 |
|
147 | rhs n = HOLogic.mk_conj (P n, rhs (n - 1)) |
|
148 |
|
149 fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n) |
|
150 | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp |
|
151 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n) |
|
152 |
|
153 fun de_bruijn n = |
|
154 HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n)) |
|
155 *} |
144 |
156 |
145 use "output_tutorial.ML" |
157 use "output_tutorial.ML" |
146 use "antiquote_setup.ML" |
158 use "antiquote_setup.ML" |
147 |
159 |
148 |
160 |