313 val uterm = P.underscore >> K NONE || P.term >> SOME; |
313 val uterm = P.underscore >> K NONE || P.term >> SOME; |
314 |
314 |
315 val view_val = |
315 val view_val = |
316 Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") []; |
316 Scan.optional (P.$$$ "[" |-- Scan.repeat1 uterm --| P.$$$ "]") []; |
317 |
317 |
318 val registrationP = |
318 val interpretationP = |
319 OuterSyntax.command "registration" |
319 OuterSyntax.command "interpretation" |
320 "prove and register instance of locale expression" K.thy_goal |
320 "prove and register interpretation of locale expression" K.thy_goal |
321 ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val |
321 ((P.opt_thm_name ":" -- P.locale_expr -- P.!!! view_val |
322 >> IsarThy.register_globally) |
322 >> IsarThy.register_globally) |
323 >> (Toplevel.print oo Toplevel.theory_to_proof)); |
323 >> (Toplevel.print oo Toplevel.theory_to_proof)); |
324 |
324 |
325 |
325 |
592 val print_localeP = |
592 val print_localeP = |
593 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
593 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
594 (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
594 (locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
595 |
595 |
596 val print_registrationsP = |
596 val print_registrationsP = |
597 OuterSyntax.improper_command "print_registrations" |
597 OuterSyntax.improper_command "print_interps" |
598 "print registrations of named locale in this theory" K.diag |
598 "print interpretations of named locale in this theory" K.diag |
599 (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); |
599 (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations)); |
600 |
600 |
601 val print_attributesP = |
601 val print_attributesP = |
602 OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag |
602 OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag |
603 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); |
603 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes)); |
798 assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP, |
798 assumeP, presumeP, defP, obtainP, letP, caseP, thenP, fromP, withP, |
799 noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP, |
799 noteP, usingP, beginP, endP, nextP, qedP, terminal_proofP, |
800 default_proofP, immediate_proofP, done_proofP, skip_proofP, |
800 default_proofP, immediate_proofP, done_proofP, skip_proofP, |
801 forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP, |
801 forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP, |
802 finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP, |
802 finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP, |
803 redoP, undos_proofP, undoP, killP, registrationP, instantiateP, |
803 redoP, undos_proofP, undoP, killP, interpretationP, instantiateP, |
804 (*diagnostic commands*) |
804 (*diagnostic commands*) |
805 pretty_setmarginP, print_commandsP, print_contextP, print_theoryP, |
805 pretty_setmarginP, print_commandsP, print_contextP, print_theoryP, |
806 print_syntaxP, print_theoremsP, print_localesP, print_localeP, |
806 print_syntaxP, print_theoremsP, print_localesP, print_localeP, |
807 print_registrationsP, |
807 print_registrationsP, |
808 print_attributesP, print_rulesP, print_induct_rulesP, |
808 print_attributesP, print_rulesP, print_induct_rulesP, |