181 |
181 |
182 (* axioms and definitions *) |
182 (* axioms and definitions *) |
183 |
183 |
184 val _ = |
184 val _ = |
185 OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl |
185 OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl |
186 (Scan.repeat1 SpecParse.spec >> |
186 (Scan.repeat1 Parse_Spec.spec >> |
187 (Toplevel.theory o |
187 (Toplevel.theory o |
188 (IsarCmd.add_axioms o |
188 (IsarCmd.add_axioms o |
189 tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead")))); |
189 tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead")))); |
190 |
190 |
191 val opt_unchecked_overloaded = |
191 val opt_unchecked_overloaded = |
194 Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false); |
194 Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false); |
195 |
195 |
196 val _ = |
196 val _ = |
197 OuterSyntax.command "defs" "define constants" Keyword.thy_decl |
197 OuterSyntax.command "defs" "define constants" Keyword.thy_decl |
198 (opt_unchecked_overloaded -- |
198 (opt_unchecked_overloaded -- |
199 Scan.repeat1 (SpecParse.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y))) |
199 Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y))) |
200 >> (Toplevel.theory o IsarCmd.add_defs)); |
200 >> (Toplevel.theory o IsarCmd.add_defs)); |
201 |
201 |
202 |
202 |
203 (* old constdefs *) |
203 (* old constdefs *) |
204 |
204 |
206 Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) || |
206 Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) || |
207 Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix' |
207 Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix' |
208 --| Scan.option Parse.where_ >> Parse.triple1 || |
208 --| Scan.option Parse.where_ >> Parse.triple1 || |
209 Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2; |
209 Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2; |
210 |
210 |
211 val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- Parse.prop); |
211 val old_constdef = Scan.option old_constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop); |
212 |
212 |
213 val structs = |
213 val structs = |
214 Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure") |
214 Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure") |
215 |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) []; |
215 |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) []; |
216 |
216 |
221 |
221 |
222 (* constant definitions and abbreviations *) |
222 (* constant definitions and abbreviations *) |
223 |
223 |
224 val _ = |
224 val _ = |
225 OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl |
225 OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl |
226 (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args)); |
226 (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args)); |
227 |
227 |
228 val _ = |
228 val _ = |
229 OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl |
229 OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl |
230 (opt_mode -- (Scan.option SpecParse.constdecl -- Parse.prop) |
230 (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop) |
231 >> (fn (mode, args) => Specification.abbreviation_cmd mode args)); |
231 >> (fn (mode, args) => Specification.abbreviation_cmd mode args)); |
232 |
232 |
233 val _ = |
233 val _ = |
234 OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" |
234 OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" |
235 Keyword.thy_decl |
235 Keyword.thy_decl |
243 >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); |
243 >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); |
244 |
244 |
245 val _ = |
245 val _ = |
246 OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" |
246 OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" |
247 Keyword.thy_decl |
247 Keyword.thy_decl |
248 (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix) |
248 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix) |
249 >> (fn (mode, args) => Specification.notation_cmd true mode args)); |
249 >> (fn (mode, args) => Specification.notation_cmd true mode args)); |
250 |
250 |
251 val _ = |
251 val _ = |
252 OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" |
252 OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" |
253 Keyword.thy_decl |
253 Keyword.thy_decl |
254 (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix) |
254 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix) |
255 >> (fn (mode, args) => Specification.notation_cmd false mode args)); |
255 >> (fn (mode, args) => Specification.notation_cmd false mode args)); |
256 |
256 |
257 |
257 |
258 (* constant specifications *) |
258 (* constant specifications *) |
259 |
259 |
260 val _ = |
260 val _ = |
261 OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl |
261 OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl |
262 (Scan.optional Parse.fixes [] -- |
262 (Scan.optional Parse.fixes [] -- |
263 Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 SpecParse.specs)) [] |
263 Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) [] |
264 >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y))); |
264 >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y))); |
265 |
265 |
266 |
266 |
267 (* theorems *) |
267 (* theorems *) |
268 |
268 |
269 fun theorems kind = |
269 fun theorems kind = |
270 SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args); |
270 Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args); |
271 |
271 |
272 val _ = |
272 val _ = |
273 OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK); |
273 OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK); |
274 |
274 |
275 val _ = |
275 val _ = |
276 OuterSyntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK); |
276 OuterSyntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK); |
277 |
277 |
278 val _ = |
278 val _ = |
279 OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl |
279 OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl |
280 (Parse.and_list1 SpecParse.xthms1 |
280 (Parse.and_list1 Parse_Spec.xthms1 |
281 >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)])); |
281 >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)])); |
282 |
282 |
283 |
283 |
284 (* name space entry path *) |
284 (* name space entry path *) |
285 |
285 |
414 |
414 |
415 |
415 |
416 (* locales *) |
416 (* locales *) |
417 |
417 |
418 val locale_val = |
418 val locale_val = |
419 SpecParse.locale_expression false -- |
419 Parse_Spec.locale_expression false -- |
420 Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
420 Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || |
421 Scan.repeat1 SpecParse.context_element >> pair ([], []); |
421 Scan.repeat1 Parse_Spec.context_element >> pair ([], []); |
422 |
422 |
423 val _ = |
423 val _ = |
424 OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl |
424 OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl |
425 (Parse.binding -- |
425 (Parse.binding -- |
426 Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin |
426 Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin |
430 |
430 |
431 val _ = |
431 val _ = |
432 OuterSyntax.command "sublocale" |
432 OuterSyntax.command "sublocale" |
433 "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal |
433 "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal |
434 (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") -- |
434 (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") -- |
435 Parse.!!! (SpecParse.locale_expression false) |
435 Parse.!!! (Parse_Spec.locale_expression false) |
436 >> (fn (loc, expr) => |
436 >> (fn (loc, expr) => |
437 Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))); |
437 Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))); |
438 |
438 |
439 val _ = |
439 val _ = |
440 OuterSyntax.command "interpretation" |
440 OuterSyntax.command "interpretation" |
441 "prove interpretation of locale expression in theory" Keyword.thy_goal |
441 "prove interpretation of locale expression in theory" Keyword.thy_goal |
442 (Parse.!!! (SpecParse.locale_expression true) -- |
442 (Parse.!!! (Parse_Spec.locale_expression true) -- |
443 Scan.optional (Parse.where_ |-- Parse.and_list1 (SpecParse.opt_thm_name ":" -- Parse.prop)) [] |
443 Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [] |
444 >> (fn (expr, equations) => Toplevel.print o |
444 >> (fn (expr, equations) => Toplevel.print o |
445 Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations))); |
445 Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations))); |
446 |
446 |
447 val _ = |
447 val _ = |
448 OuterSyntax.command "interpret" |
448 OuterSyntax.command "interpret" |
449 "prove interpretation of locale expression in proof context" |
449 "prove interpretation of locale expression in proof context" |
450 (Keyword.tag_proof Keyword.prf_goal) |
450 (Keyword.tag_proof Keyword.prf_goal) |
451 (Parse.!!! (SpecParse.locale_expression true) |
451 (Parse.!!! (Parse_Spec.locale_expression true) |
452 >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr))); |
452 >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr))); |
453 |
453 |
454 |
454 |
455 (* classes *) |
455 (* classes *) |
456 |
456 |
457 val class_val = |
457 val class_val = |
458 SpecParse.class_expr -- |
458 Parse_Spec.class_expr -- |
459 Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] || |
459 Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] || |
460 Scan.repeat1 SpecParse.context_element >> pair []; |
460 Scan.repeat1 Parse_Spec.context_element >> pair []; |
461 |
461 |
462 val _ = |
462 val _ = |
463 OuterSyntax.command "class" "define type class" Keyword.thy_decl |
463 OuterSyntax.command "class" "define type class" Keyword.thy_decl |
464 (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin |
464 (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin |
465 >> (fn ((name, (supclasses, elems)), begin) => |
465 >> (fn ((name, (supclasses, elems)), begin) => |
512 fun gen_theorem schematic kind = |
512 fun gen_theorem schematic kind = |
513 OuterSyntax.local_theory_to_proof' |
513 OuterSyntax.local_theory_to_proof' |
514 (if schematic then "schematic_" ^ kind else kind) |
514 (if schematic then "schematic_" ^ kind else kind) |
515 ("state " ^ (if schematic then "schematic " ^ kind else kind)) |
515 ("state " ^ (if schematic then "schematic " ^ kind else kind)) |
516 (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal) |
516 (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal) |
517 (Scan.optional (SpecParse.opt_thm_name ":" --| |
517 (Scan.optional (Parse_Spec.opt_thm_name ":" --| |
518 Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding -- |
518 Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding -- |
519 SpecParse.general_statement >> (fn (a, (elems, concl)) => |
519 Parse_Spec.general_statement >> (fn (a, (elems, concl)) => |
520 ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) |
520 ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) |
521 kind NONE (K I) a elems concl))); |
521 kind NONE (K I) a elems concl))); |
522 |
522 |
523 val _ = gen_theorem false Thm.theoremK; |
523 val _ = gen_theorem false Thm.theoremK; |
524 val _ = gen_theorem false Thm.lemmaK; |
524 val _ = gen_theorem false Thm.lemmaK; |
535 Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward)); |
535 Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward)); |
536 |
536 |
537 val _ = |
537 val _ = |
538 OuterSyntax.command "have" "state local goal" |
538 OuterSyntax.command "have" "state local goal" |
539 (Keyword.tag_proof Keyword.prf_goal) |
539 (Keyword.tag_proof Keyword.prf_goal) |
540 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); |
540 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); |
541 |
541 |
542 val _ = |
542 val _ = |
543 OuterSyntax.command "hence" "abbreviates \"then have\"" |
543 OuterSyntax.command "hence" "abbreviates \"then have\"" |
544 (Keyword.tag_proof Keyword.prf_goal) |
544 (Keyword.tag_proof Keyword.prf_goal) |
545 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); |
545 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence)); |
546 |
546 |
547 val _ = |
547 val _ = |
548 OuterSyntax.command "show" "state local goal, solving current obligation" |
548 OuterSyntax.command "show" "state local goal, solving current obligation" |
549 (Keyword.tag_proof Keyword.prf_asm_goal) |
549 (Keyword.tag_proof Keyword.prf_asm_goal) |
550 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); |
550 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show)); |
551 |
551 |
552 val _ = |
552 val _ = |
553 OuterSyntax.command "thus" "abbreviates \"then show\"" |
553 OuterSyntax.command "thus" "abbreviates \"then show\"" |
554 (Keyword.tag_proof Keyword.prf_asm_goal) |
554 (Keyword.tag_proof Keyword.prf_asm_goal) |
555 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); |
555 (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus)); |
556 |
556 |
557 |
557 |
558 (* facts *) |
558 (* facts *) |
559 |
559 |
560 val facts = Parse.and_list1 SpecParse.xthms1; |
560 val facts = Parse.and_list1 Parse_Spec.xthms1; |
561 |
561 |
562 val _ = |
562 val _ = |
563 OuterSyntax.command "then" "forward chaining" |
563 OuterSyntax.command "then" "forward chaining" |
564 (Keyword.tag_proof Keyword.prf_chain) |
564 (Keyword.tag_proof Keyword.prf_chain) |
565 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); |
565 (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain)); |
575 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd))); |
575 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd))); |
576 |
576 |
577 val _ = |
577 val _ = |
578 OuterSyntax.command "note" "define facts" |
578 OuterSyntax.command "note" "define facts" |
579 (Keyword.tag_proof Keyword.prf_decl) |
579 (Keyword.tag_proof Keyword.prf_decl) |
580 (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd))); |
580 (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd))); |
581 |
581 |
582 val _ = |
582 val _ = |
583 OuterSyntax.command "using" "augment goal facts" |
583 OuterSyntax.command "using" "augment goal facts" |
584 (Keyword.tag_proof Keyword.prf_decl) |
584 (Keyword.tag_proof Keyword.prf_decl) |
585 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd))); |
585 (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd))); |
598 (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd))); |
598 (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd))); |
599 |
599 |
600 val _ = |
600 val _ = |
601 OuterSyntax.command "assume" "assume propositions" |
601 OuterSyntax.command "assume" "assume propositions" |
602 (Keyword.tag_proof Keyword.prf_asm) |
602 (Keyword.tag_proof Keyword.prf_asm) |
603 (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd))); |
603 (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd))); |
604 |
604 |
605 val _ = |
605 val _ = |
606 OuterSyntax.command "presume" "assume propositions, to be established later" |
606 OuterSyntax.command "presume" "assume propositions, to be established later" |
607 (Keyword.tag_proof Keyword.prf_asm) |
607 (Keyword.tag_proof Keyword.prf_asm) |
608 (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd))); |
608 (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd))); |
609 |
609 |
610 val _ = |
610 val _ = |
611 OuterSyntax.command "def" "local definition" |
611 OuterSyntax.command "def" "local definition" |
612 (Keyword.tag_proof Keyword.prf_asm) |
612 (Keyword.tag_proof Keyword.prf_asm) |
613 (Parse.and_list1 |
613 (Parse.and_list1 |
614 (SpecParse.opt_thm_name ":" -- |
614 (Parse_Spec.opt_thm_name ":" -- |
615 ((Parse.binding -- Parse.opt_mixfix) -- |
615 ((Parse.binding -- Parse.opt_mixfix) -- |
616 ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp))) |
616 ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp))) |
617 >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd))); |
617 >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd))); |
618 |
618 |
619 val _ = |
619 val _ = |
620 OuterSyntax.command "obtain" "generalized existence" |
620 OuterSyntax.command "obtain" "generalized existence" |
621 (Keyword.tag_proof Keyword.prf_asm_goal) |
621 (Keyword.tag_proof Keyword.prf_asm_goal) |
622 (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- SpecParse.statement |
622 (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement |
623 >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z))); |
623 >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z))); |
624 |
624 |
625 val _ = |
625 val _ = |
626 OuterSyntax.command "guess" "wild guessing (unstructured)" |
626 OuterSyntax.command "guess" "wild guessing (unstructured)" |
627 (Keyword.tag_proof Keyword.prf_asm_goal) |
627 (Keyword.tag_proof Keyword.prf_asm_goal) |
634 >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd))); |
634 >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd))); |
635 |
635 |
636 val _ = |
636 val _ = |
637 OuterSyntax.command "write" "add concrete syntax for constants / fixed variables" |
637 OuterSyntax.command "write" "add concrete syntax for constants / fixed variables" |
638 (Keyword.tag_proof Keyword.prf_decl) |
638 (Keyword.tag_proof Keyword.prf_decl) |
639 (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix) |
639 (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix) |
640 >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args))); |
640 >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args))); |
641 |
641 |
642 val case_spec = |
642 val case_spec = |
643 (Parse.$$$ "(" |-- |
643 (Parse.$$$ "(" |-- |
644 Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") || |
644 Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") || |
645 Parse.xname >> rpair []) -- SpecParse.opt_attribs >> Parse.triple1; |
645 Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1; |
646 |
646 |
647 val _ = |
647 val _ = |
648 OuterSyntax.command "case" "invoke local context" |
648 OuterSyntax.command "case" "invoke local context" |
649 (Keyword.tag_proof Keyword.prf_asm) |
649 (Keyword.tag_proof Keyword.prf_asm) |
650 (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd))); |
650 (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd))); |
881 OuterSyntax.improper_command "class_deps" "visualize class dependencies" |
881 OuterSyntax.improper_command "class_deps" "visualize class dependencies" |
882 Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); |
882 Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); |
883 |
883 |
884 val _ = |
884 val _ = |
885 OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" |
885 OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" |
886 Keyword.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); |
886 Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); |
887 |
887 |
888 val _ = |
888 val _ = |
889 OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag |
889 OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag |
890 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); |
890 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds)); |
891 |
891 |
897 OuterSyntax.improper_command "print_cases" "print cases of proof context" Keyword.diag |
897 OuterSyntax.improper_command "print_cases" "print cases of proof context" Keyword.diag |
898 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); |
898 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases)); |
899 |
899 |
900 val _ = |
900 val _ = |
901 OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag |
901 OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag |
902 (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); |
902 (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts)); |
903 |
903 |
904 val _ = |
904 val _ = |
905 OuterSyntax.improper_command "thm" "print theorems" Keyword.diag |
905 OuterSyntax.improper_command "thm" "print theorems" Keyword.diag |
906 (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); |
906 (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); |
907 |
907 |
908 val _ = |
908 val _ = |
909 OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag |
909 OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag |
910 (opt_modes -- Scan.option SpecParse.xthms1 |
910 (opt_modes -- Scan.option Parse_Spec.xthms1 |
911 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); |
911 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); |
912 |
912 |
913 val _ = |
913 val _ = |
914 OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag |
914 OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag |
915 (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); |
915 (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); |
916 |
916 |
917 val _ = |
917 val _ = |
918 OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag |
918 OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag |
919 (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); |
919 (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); |
920 |
920 |