221 (P.opt_locale_target -- opt_mode -- |
221 (P.opt_locale_target -- opt_mode -- |
222 Scan.repeat1 (Scan.option constdecl -- P.prop) |
222 Scan.repeat1 (Scan.option constdecl -- P.prop) |
223 >> (fn ((loc, mode), args) => |
223 >> (fn ((loc, mode), args) => |
224 Toplevel.local_theory loc (Specification.abbreviation mode args))); |
224 Toplevel.local_theory loc (Specification.abbreviation mode args))); |
225 |
225 |
226 val const_syntaxP = |
226 val notationP = |
227 OuterSyntax.command "const_syntax" "constant syntax" K.thy_decl |
227 OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl |
228 (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix) |
228 (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix) |
229 >> (fn ((loc, mode), args) => |
229 >> (fn ((loc, mode), args) => |
230 Toplevel.local_theory loc (Specification.const_syntax mode args))); |
230 Toplevel.local_theory loc (Specification.notation mode args))); |
231 |
231 |
232 |
232 |
233 (* constant specifications *) |
233 (* constant specifications *) |
234 |
234 |
235 val axiomatizationP = |
235 val axiomatizationP = |
903 text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, |
903 text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP, |
904 (*theory sections*) |
904 (*theory sections*) |
905 classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP, |
905 classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP, |
906 nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP, |
906 nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP, |
907 no_syntaxP, translationsP, no_translationsP, axiomsP, defsP, |
907 no_syntaxP, translationsP, no_translationsP, axiomsP, defsP, |
908 constdefsP, definitionP, abbreviationP, const_syntaxP, |
908 constdefsP, definitionP, abbreviationP, notationP, axiomatizationP, |
909 axiomatizationP, theoremsP, lemmasP, declareP, globalP, localP, |
909 theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP, |
910 hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP, |
910 ml_commandP, ml_setupP, setupP, method_setupP, |
911 parse_ast_translationP, parse_translationP, print_translationP, |
911 parse_ast_translationP, parse_translationP, print_translationP, |
912 typed_print_translationP, print_ast_translationP, |
912 typed_print_translationP, print_ast_translationP, |
913 token_translationP, oracleP, localeP, |
913 token_translationP, oracleP, localeP, |
914 (*proof commands*) |
914 (*proof commands*) |
915 theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, |
915 theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, |