equal
deleted
inserted
replaced
93 |
93 |
94 |
94 |
95 (* concrete syntax *) |
95 (* concrete syntax *) |
96 |
96 |
97 val _ = Theory.setup |
97 val _ = Theory.setup |
98 (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del) |
98 (Attrib.setup @{binding trans} (Attrib.add_del trans_add trans_del) |
99 "declaration of transitivity rule" #> |
99 "declaration of transitivity rule" #> |
100 Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del) |
100 Attrib.setup @{binding sym} (Attrib.add_del sym_add sym_del) |
101 "declaration of symmetry rule" #> |
101 "declaration of symmetry rule" #> |
102 Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric) |
102 Attrib.setup @{binding symmetric} (Scan.succeed symmetric) |
103 "resolution with symmetry rule" #> |
103 "resolution with symmetry rule" #> |
104 Global_Theory.add_thms |
104 Global_Theory.add_thms |
105 [((Binding.empty, transitive_thm), [trans_add]), |
105 [((Binding.empty, transitive_thm), [trans_add]), |
106 ((Binding.empty, symmetric_thm), [sym_add])] #> snd); |
106 ((Binding.empty, symmetric_thm), [sym_add])] #> snd); |
107 |
107 |
195 in maintain_calculation int final calc state end; |
195 in maintain_calculation int final calc state end; |
196 |
196 |
197 val moreover = collect false; |
197 val moreover = collect false; |
198 val ultimately = collect true; |
198 val ultimately = collect true; |
199 |
199 |
|
200 |
|
201 (* outer syntax *) |
|
202 |
|
203 val calc_args = |
|
204 Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"}))); |
|
205 |
|
206 val _ = |
|
207 Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts" |
|
208 (calc_args >> (Toplevel.proofs' o also_cmd)); |
|
209 |
|
210 val _ = |
|
211 Outer_Syntax.command @{command_spec "finally"} |
|
212 "combine calculation and current facts, exhibit result" |
|
213 (calc_args >> (Toplevel.proofs' o finally_cmd)); |
|
214 |
|
215 val _ = |
|
216 Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts" |
|
217 (Scan.succeed (Toplevel.proof' moreover)); |
|
218 |
|
219 val _ = |
|
220 Outer_Syntax.command @{command_spec "ultimately"} |
|
221 "augment calculation by current facts, exhibit result" |
|
222 (Scan.succeed (Toplevel.proof' ultimately)); |
|
223 |
|
224 val _ = |
|
225 Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules" |
|
226 (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of))); |
|
227 |
200 end; |
228 end; |