src/Pure/Isar/isar_syn.ML
author haftmann
Sat Feb 10 09:26:18 2007 +0100 (2007-02-10 ago)
changeset 22299 a1293efe7ea5
parent 22239 9ddd3349d597
child 22321 e5cddafe2629
permissions -rw-r--r--
moved commands of class package here
     1 (*  Title:      Pure/Isar/isar_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar/Pure outer syntax.
     6 *)
     7 
     8 structure IsarSyn: sig end =
     9 struct
    10 
    11 structure P = OuterParse and K = OuterKeyword;
    12 
    13 
    14 (** init and exit **)
    15 
    16 val theoryP =
    17   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
    18     (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory));
    19 
    20 val endP =
    21   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
    22     (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
    23 
    24 
    25 (** markup commands **)
    26 
    27 val headerP = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
    28   (P.position P.text >> IsarCmd.add_header);
    29 
    30 val chapterP = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
    31   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter);
    32 
    33 val sectionP = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
    34   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section);
    35 
    36 val subsectionP = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
    37   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection);
    38 
    39 val subsubsectionP =
    40   OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
    41   K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection);
    42 
    43 val textP = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
    44   K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text);
    45 
    46 val text_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw"
    47   "raw document preparation text"
    48   K.thy_decl (P.position P.text >> IsarCmd.add_text_raw);
    49 
    50 val sectP = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
    51   (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect);
    52 
    53 val subsectP = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
    54   (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect);
    55 
    56 val subsubsectP = OuterSyntax.markup_command ThyOutput.Markup "subsubsect"
    57   "formal comment (proof)" (K.tag_proof K.prf_heading)
    58   (P.position P.text >> IsarCmd.add_subsubsect);
    59 
    60 val txtP = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
    61   (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt);
    62 
    63 val txt_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
    64   "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
    65   (P.position P.text >> IsarCmd.add_txt_raw);
    66 
    67 
    68 
    69 (** theory sections **)
    70 
    71 (* classes and sorts *)
    72 
    73 val classesP =
    74   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    75     (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    76         P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class));
    77 
    78 val classrelP =
    79   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    80     (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
    81     >> (Toplevel.theory o AxClass.axiomatize_classrel));
    82 
    83 val defaultsortP =
    84   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    85     (P.sort >> (Toplevel.theory o Theory.add_defsort));
    86 
    87 val axclassP =
    88   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
    89     (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    90         P.!!! (P.list1 P.xname)) []
    91         -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
    92         -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    93       >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    94 
    95 
    96 (* types *)
    97 
    98 val typedeclP =
    99   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
   100     (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
   101       Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
   102 
   103 val typeabbrP =
   104   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   105     (Scan.repeat1
   106       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
   107       >> (Toplevel.theory o Theory.add_tyabbrs o
   108         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   109 
   110 val nontermP =
   111   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   112     K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
   113 
   114 val aritiesP =
   115   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   116     (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
   117       >> (Toplevel.theory o fold AxClass.axiomatize_arity));
   118 
   119 
   120 (* consts and syntax *)
   121 
   122 val judgmentP =
   123   OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
   124     (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
   125 
   126 val constsP =
   127   OuterSyntax.command "consts" "declare constants" K.thy_decl
   128     (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
   129 
   130 val opt_overloaded = P.opt_keyword "overloaded";
   131 
   132 val finalconstsP =
   133   OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
   134     (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
   135 
   136 val mode_spec =
   137   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
   138 
   139 val opt_mode =
   140   Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
   141 
   142 val syntaxP =
   143   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   144     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   145 
   146 val no_syntaxP =
   147   OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
   148     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax));
   149 
   150 
   151 (* translations *)
   152 
   153 val trans_pat =
   154   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   155 
   156 fun trans_arrow toks =
   157   ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
   158     (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
   159     (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
   160 
   161 val trans_line =
   162   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   163     >> (fn (left, (arr, right)) => arr (left, right));
   164 
   165 val translationsP =
   166   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   167     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   168 
   169 val no_translationsP =
   170   OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
   171     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules));
   172 
   173 
   174 (* axioms and definitions *)
   175 
   176 val axiomsP =
   177   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   178     (Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
   179 
   180 val opt_unchecked_overloaded =
   181   Scan.optional (P.$$$ "(" |-- P.!!!
   182     (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
   183       P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
   184 
   185 val defsP =
   186   OuterSyntax.command "defs" "define constants" K.thy_decl
   187     (opt_unchecked_overloaded -- Scan.repeat1 SpecParse.spec_name
   188       >> (Toplevel.theory o IsarCmd.add_defs));
   189 
   190 
   191 (* old constdefs *)
   192 
   193 val old_constdecl =
   194   P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
   195   P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
   196     --| Scan.option P.where_ >> P.triple1 ||
   197   P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
   198 
   199 val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   200 
   201 val structs =
   202   Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
   203 
   204 val constdefsP =
   205   OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
   206     (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
   207 
   208 
   209 (* constant definitions and abbreviations *)
   210 
   211 val constdecl =
   212   P.name --
   213     (P.where_ >> K (NONE, NoSyn) ||
   214       P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
   215       Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
   216   >> P.triple2;
   217 
   218 val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   219 
   220 val definitionP =
   221   OuterSyntax.command "definition" "constant definition" K.thy_decl
   222     (P.opt_target -- constdef
   223     >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
   224 
   225 val abbreviationP =
   226   OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
   227     (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
   228     >> (fn ((loc, mode), args) =>
   229         Toplevel.local_theory loc (Specification.abbreviation mode args)));
   230 
   231 val notationP =
   232   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
   233     (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   234     >> (fn ((loc, mode), args) =>
   235         Toplevel.local_theory loc (Specification.notation mode args)));
   236 
   237 
   238 (* constant specifications *)
   239 
   240 val axiomatizationP =
   241   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
   242     (P.opt_target --
   243      (Scan.optional P.fixes [] --
   244       Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
   245     >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
   246 
   247 
   248 (* theorems *)
   249 
   250 fun theorems kind = P.opt_target -- SpecParse.name_facts
   251   >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
   252 
   253 val theoremsP =
   254   OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
   255 
   256 val lemmasP =
   257   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
   258 
   259 val declareP =
   260   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
   261     (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
   262       >> (fn (loc, args) => Toplevel.local_theory loc
   263           (#2 o Specification.theorems "" [(("", []), args)])));
   264 
   265 
   266 (* name space entry path *)
   267 
   268 val globalP =
   269   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   270     (Scan.succeed (Toplevel.theory Sign.root_path));
   271 
   272 val localP =
   273   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   274     (Scan.succeed (Toplevel.theory Sign.local_path));
   275 
   276 val hideP =
   277   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
   278     ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
   279       (Toplevel.theory o uncurry Sign.hide_names));
   280 
   281 
   282 (* use ML text *)
   283 
   284 val useP =
   285   OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag)
   286     (P.path >> (Toplevel.no_timing oo IsarCmd.use));
   287 
   288 val mlP =
   289   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
   290     (P.text >> IsarCmd.use_mltext true);
   291 
   292 val ml_commandP =
   293   OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
   294     (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
   295 
   296 val ml_setupP =
   297   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
   298     (P.text >> IsarCmd.use_mltext_theory);
   299 
   300 val setupP =
   301   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
   302     (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup));
   303 
   304 val method_setupP =
   305   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
   306     (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
   307       >> (Toplevel.theory o Method.method_setup));
   308 
   309 val declarationP =
   310   OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
   311     (P.opt_target -- P.text
   312     >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
   313 
   314 val simproc_setupP =
   315   OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
   316     (P.opt_target --
   317       P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
   318       Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
   319     >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
   320 
   321 
   322 (* translation functions *)
   323 
   324 val trfun = P.opt_keyword "advanced" -- P.text;
   325 
   326 val parse_ast_translationP =
   327   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   328     (K.tag_ml K.thy_decl)
   329     (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
   330 
   331 val parse_translationP =
   332   OuterSyntax.command "parse_translation" "install parse translation functions"
   333     (K.tag_ml K.thy_decl)
   334     (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
   335 
   336 val print_translationP =
   337   OuterSyntax.command "print_translation" "install print translation functions"
   338     (K.tag_ml K.thy_decl)
   339     (trfun >> (Toplevel.theory o IsarCmd.print_translation));
   340 
   341 val typed_print_translationP =
   342   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   343     (K.tag_ml K.thy_decl)
   344     (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
   345 
   346 val print_ast_translationP =
   347   OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   348     (K.tag_ml K.thy_decl)
   349     (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
   350 
   351 val token_translationP =
   352   OuterSyntax.command "token_translation" "install token translation functions"
   353     (K.tag_ml K.thy_decl)
   354     (P.text >> (Toplevel.theory o IsarCmd.token_translation));
   355 
   356 
   357 (* oracles *)
   358 
   359 val oracleP =
   360   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
   361     (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
   362       -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
   363 
   364 
   365 (* local theories *)
   366 
   367 val contextP =
   368   OuterSyntax.command "context" "enter local theory context" K.thy_decl
   369     (P.name --| P.begin >> (fn name =>
   370       Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
   371 
   372 
   373 (* locales *)
   374 
   375 val locale_val =
   376   (SpecParse.locale_expr --
   377     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   378   Scan.repeat1 SpecParse.context_element >> pair Locale.empty);
   379 
   380 val localeP =
   381   OuterSyntax.command "locale" "define named proof context" K.thy_decl
   382     ((P.opt_keyword "open" >> not) -- P.name
   383         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
   384         -- P.opt_begin
   385       >> (fn (((is_open, name), (expr, elems)), begin) =>
   386           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   387             (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false)));
   388 
   389 val interpretationP =
   390   OuterSyntax.command "interpretation"
   391     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
   392     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
   393       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
   394       SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts >> (fn ((x, y), z) =>
   395         Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I x y z)));
   396 
   397 val interpretP =
   398   OuterSyntax.command "interpret"
   399     "prove and register interpretation of locale expression in proof context"
   400     (K.tag_proof K.prf_goal)
   401     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   402       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z)));
   403 
   404 
   405 (* classes *)
   406 
   407 local
   408 
   409 val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
   410 
   411 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
   412 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
   413 
   414 val parse_arity =
   415   (P.xname --| P.$$$ "::" -- P.!!! P.arity)
   416     >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
   417 
   418 in
   419 
   420 val classP =
   421   OuterSyntax.command classK "define type class" K.thy_decl (
   422     P.name --| P.$$$ "="
   423     -- (
   424       class_subP --| P.$$$ "+" -- class_bodyP
   425       || class_subP >> rpair []
   426       || class_bodyP >> pair [])
   427     -- P.opt_begin
   428     >> (fn ((bname, (supclasses, elems)), begin) =>
   429         Toplevel.begin_local_theory begin
   430           (ClassPackage.class_e bname supclasses elems #-> TheoryTarget.begin true)));
   431 
   432 val instanceP =
   433   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
   434       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   435            >> ClassPackage.instance_sort_e
   436       || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
   437            >> (fn (arities, defs) => ClassPackage.instance_arity_e arities defs)
   438     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   439 
   440 val print_classesP =
   441   OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
   442     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
   443       o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
   444 
   445 end;
   446 
   447 
   448 
   449 (** proof commands **)
   450 
   451 (* statements *)
   452 
   453 fun gen_theorem kind =
   454   OuterSyntax.command kind ("state " ^ kind) K.thy_goal
   455     (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
   456       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
   457       SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
   458       (Toplevel.print o
   459        Toplevel.local_theory_to_proof loc
   460          (Specification.theorem kind NONE (K I) a elems concl))));
   461 
   462 val theoremP = gen_theorem Thm.theoremK;
   463 val lemmaP = gen_theorem Thm.lemmaK;
   464 val corollaryP = gen_theorem Thm.corollaryK;
   465 
   466 val haveP =
   467   OuterSyntax.command "have" "state local goal"
   468     (K.tag_proof K.prf_goal)
   469     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   470 
   471 val henceP =
   472   OuterSyntax.command "hence" "abbreviates \"then have\""
   473     (K.tag_proof K.prf_goal)
   474     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   475 
   476 val showP =
   477   OuterSyntax.command "show" "state local goal, solving current obligation"
   478     (K.tag_proof K.prf_asm_goal)
   479     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   480 
   481 val thusP =
   482   OuterSyntax.command "thus" "abbreviates \"then show\""
   483     (K.tag_proof K.prf_asm_goal)
   484     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   485 
   486 
   487 (* facts *)
   488 
   489 val facts = P.and_list1 SpecParse.xthms1;
   490 
   491 val thenP =
   492   OuterSyntax.command "then" "forward chaining"
   493     (K.tag_proof K.prf_chain)
   494     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
   495 
   496 val fromP =
   497   OuterSyntax.command "from" "forward chaining from given facts"
   498     (K.tag_proof K.prf_chain)
   499     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
   500 
   501 val withP =
   502   OuterSyntax.command "with" "forward chaining from given and current facts"
   503     (K.tag_proof K.prf_chain)
   504     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
   505 
   506 val noteP =
   507   OuterSyntax.command "note" "define facts"
   508     (K.tag_proof K.prf_decl)
   509     (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
   510 
   511 val usingP =
   512   OuterSyntax.command "using" "augment goal facts"
   513     (K.tag_proof K.prf_decl)
   514     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
   515 
   516 val unfoldingP =
   517   OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
   518     (K.tag_proof K.prf_decl)
   519     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
   520 
   521 
   522 (* proof context *)
   523 
   524 val fixP =
   525   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
   526     (K.tag_proof K.prf_asm)
   527     (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
   528 
   529 val assumeP =
   530   OuterSyntax.command "assume" "assume propositions"
   531     (K.tag_proof K.prf_asm)
   532     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
   533 
   534 val presumeP =
   535   OuterSyntax.command "presume" "assume propositions, to be established later"
   536     (K.tag_proof K.prf_asm)
   537     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
   538 
   539 val defP =
   540   OuterSyntax.command "def" "local definition"
   541     (K.tag_proof K.prf_asm)
   542     (P.and_list1
   543       (SpecParse.opt_thm_name ":" --
   544         ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   545     >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
   546 
   547 val obtainP =
   548   OuterSyntax.command "obtain" "generalized existence"
   549     (K.tag_proof K.prf_asm_goal)
   550     (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
   551       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
   552 
   553 val guessP =
   554   OuterSyntax.command "guess" "wild guessing (unstructured)"
   555     (K.tag_proof K.prf_asm_goal)
   556     (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
   557 
   558 val letP =
   559   OuterSyntax.command "let" "bind text variables"
   560     (K.tag_proof K.prf_decl)
   561     (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
   562       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
   563 
   564 val case_spec =
   565   (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   566     P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
   567 
   568 val caseP =
   569   OuterSyntax.command "case" "invoke local context"
   570     (K.tag_proof K.prf_asm)
   571     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
   572 
   573 
   574 (* proof structure *)
   575 
   576 val begin_blockP =
   577   OuterSyntax.command "{" "begin explicit proof block"
   578     (K.tag_proof K.prf_open)
   579     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
   580 
   581 val end_blockP =
   582   OuterSyntax.command "}" "end explicit proof block"
   583     (K.tag_proof K.prf_close)
   584     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
   585 
   586 val nextP =
   587   OuterSyntax.command "next" "enter next proof block"
   588     (K.tag_proof K.prf_block)
   589     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
   590 
   591 
   592 (* end proof *)
   593 
   594 val qedP =
   595   OuterSyntax.command "qed" "conclude (sub-)proof"
   596     (K.tag_proof K.qed_block)
   597     (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed));
   598 
   599 val terminal_proofP =
   600   OuterSyntax.command "by" "terminal backward proof"
   601     (K.tag_proof K.qed)
   602     (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof));
   603 
   604 val default_proofP =
   605   OuterSyntax.command ".." "default proof"
   606     (K.tag_proof K.qed)
   607     (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof));
   608 
   609 val immediate_proofP =
   610   OuterSyntax.command "." "immediate proof"
   611     (K.tag_proof K.qed)
   612     (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof));
   613 
   614 val done_proofP =
   615   OuterSyntax.command "done" "done proof"
   616     (K.tag_proof K.qed)
   617     (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
   618 
   619 val skip_proofP =
   620   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
   621     (K.tag_proof K.qed)
   622     (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
   623 
   624 val forget_proofP =
   625   OuterSyntax.command "oops" "forget proof"
   626     (K.tag_proof K.qed_global)
   627     (Scan.succeed Toplevel.forget_proof);
   628 
   629 
   630 (* proof steps *)
   631 
   632 val deferP =
   633   OuterSyntax.command "defer" "shuffle internal proof state"
   634     (K.tag_proof K.prf_script)
   635     (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
   636 
   637 val preferP =
   638   OuterSyntax.command "prefer" "shuffle internal proof state"
   639     (K.tag_proof K.prf_script)
   640     (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
   641 
   642 val applyP =
   643   OuterSyntax.command "apply" "initial refinement step (unstructured)"
   644     (K.tag_proof K.prf_script)
   645     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
   646 
   647 val apply_endP =
   648   OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
   649     (K.tag_proof K.prf_script)
   650     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
   651 
   652 val proofP =
   653   OuterSyntax.command "proof" "backward proof"
   654     (K.tag_proof K.prf_block)
   655     (Scan.option Method.parse >> (fn m => Toplevel.print o
   656       Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o
   657       Toplevel.skip_proof (History.apply (fn i => i + 1))));
   658 
   659 
   660 (* calculational proof commands *)
   661 
   662 val calc_args =
   663   Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
   664 
   665 val alsoP =
   666   OuterSyntax.command "also" "combine calculation and current facts"
   667     (K.tag_proof K.prf_decl)
   668     (calc_args >> (Toplevel.proofs' o Calculation.also));
   669 
   670 val finallyP =
   671   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
   672     (K.tag_proof K.prf_chain)
   673     (calc_args >> (Toplevel.proofs' o Calculation.finally));
   674 
   675 val moreoverP =
   676   OuterSyntax.command "moreover" "augment calculation by current facts"
   677     (K.tag_proof K.prf_decl)
   678     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   679 
   680 val ultimatelyP =
   681   OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
   682     (K.tag_proof K.prf_chain)
   683     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   684 
   685 
   686 (* proof navigation *)
   687 
   688 val backP =
   689   OuterSyntax.command "back" "backtracking of proof command"
   690     (K.tag_proof K.prf_script)
   691     (Scan.succeed (Toplevel.print o IsarCmd.back));
   692 
   693 
   694 (* history *)
   695 
   696 val cannot_undoP =
   697   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   698     (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
   699 
   700 val redoP =
   701   OuterSyntax.improper_command "redo" "redo last command" K.control
   702     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
   703 
   704 val undos_proofP =
   705   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   706     (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof));
   707 
   708 val undoP =
   709   OuterSyntax.improper_command "undo" "undo last command" K.control
   710     (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.undo));
   711 
   712 val killP =
   713   OuterSyntax.improper_command "kill" "kill current history node" K.control
   714     (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill));
   715 
   716 
   717 
   718 (** diagnostic commands (for interactive mode only) **)
   719 
   720 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   721 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
   722 
   723 val pretty_setmarginP =
   724   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
   725     K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   726 
   727 val helpP =
   728   OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
   729     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   730 
   731 val print_commandsP =
   732   OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
   733     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   734 
   735 val print_contextP =
   736   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
   737     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
   738 
   739 val print_theoryP =
   740   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   741     (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
   742 
   743 val print_syntaxP =
   744   OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
   745     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
   746 
   747 val print_abbrevsP =
   748   OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
   749     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
   750 
   751 val print_theoremsP =
   752   OuterSyntax.improper_command "print_theorems"
   753       "print theorems of local theory or proof context" K.diag
   754     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
   755 
   756 val print_localesP =
   757   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
   758     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
   759 
   760 val print_localeP =
   761   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
   762     (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
   763 
   764 val print_registrationsP =
   765   OuterSyntax.improper_command "print_interps"
   766     "print interpretations of named locale" K.diag
   767     (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
   768       >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
   769 
   770 val print_attributesP =
   771   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
   772     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
   773 
   774 val print_simpsetP =
   775   OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
   776     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
   777 
   778 val print_rulesP =
   779   OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
   780     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
   781 
   782 val print_induct_rulesP =
   783   OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag
   784     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules));
   785 
   786 val print_trans_rulesP =
   787   OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
   788     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
   789 
   790 val print_methodsP =
   791   OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag
   792     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
   793 
   794 val print_antiquotationsP =
   795   OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
   796     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   797 
   798 val class_depsP =
   799   OuterSyntax.improper_command "class_deps" "visualize class dependencies"
   800     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
   801 
   802 val thm_depsP =
   803   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   804     K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   805 
   806 val criterion =
   807   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
   808   P.reserved "intro" >> K FindTheorems.Intro ||
   809   P.reserved "elim" >> K FindTheorems.Elim ||
   810   P.reserved "dest" >> K FindTheorems.Dest ||
   811   P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
   812   P.term >> FindTheorems.Pattern;
   813 
   814 val find_theoremsP =
   815   OuterSyntax.improper_command "find_theorems"
   816     "print theorems meeting specified criteria" K.diag
   817     (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
   818      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   819       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
   820 
   821 val print_bindsP =
   822   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   823     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   824 
   825 val print_factsP =
   826   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
   827     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
   828 
   829 val print_casesP =
   830   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
   831     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
   832 
   833 val print_stmtsP =
   834   OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
   835     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   836 
   837 val print_thmsP =
   838   OuterSyntax.improper_command "thm" "print theorems" K.diag
   839     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   840 
   841 val print_prfsP =
   842   OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
   843     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   844 
   845 val print_full_prfsP =
   846   OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
   847     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   848 
   849 val print_propP =
   850   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   851     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
   852 
   853 val print_termP =
   854   OuterSyntax.improper_command "term" "read and print term" K.diag
   855     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
   856 
   857 val print_typeP =
   858   OuterSyntax.improper_command "typ" "read and print type" K.diag
   859     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   860 
   861 
   862 
   863 (** system commands (for interactive mode only) **)
   864 
   865 val cdP =
   866   OuterSyntax.improper_command "cd" "change current working directory" K.diag
   867     (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
   868 
   869 val pwdP =
   870   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   871     (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
   872 
   873 val use_thyP =
   874   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   875     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
   876 
   877 val use_thy_onlyP =
   878   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
   879     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only));
   880 
   881 val update_thyP =
   882   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   883     (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
   884 
   885 val update_thy_onlyP =
   886   OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
   887     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only));
   888 
   889 val touch_thyP =
   890   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
   891     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
   892 
   893 val touch_all_thysP =
   894   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
   895     (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
   896 
   897 val touch_child_thysP =
   898   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
   899     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
   900 
   901 val remove_thyP =
   902   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   903     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   904 
   905 val kill_thyP =
   906   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   907     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
   908 
   909 val display_draftsP =
   910   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
   911     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
   912 
   913 val print_draftsP =
   914   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
   915     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
   916 
   917 val opt_limits =
   918   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   919 
   920 val prP =
   921   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
   922     (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
   923 
   924 val disable_prP =
   925   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
   926     (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
   927 
   928 val enable_prP =
   929   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   930     (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
   931 
   932 val commitP =
   933   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   934     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
   935 
   936 val quitP =
   937   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   938     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
   939 
   940 val exitP =
   941   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   942     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
   943 
   944 val init_toplevelP =
   945   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
   946     (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel));
   947 
   948 val welcomeP =
   949   OuterSyntax.improper_command "welcome" "print welcome message" K.diag
   950     (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
   951 
   952 
   953 
   954 (** the Pure outer syntax **)
   955 
   956 (*keep keywords consistent with the parsers, including those in
   957   outer_parse.ML, otherwise be prepared for unexpected errors*)
   958 
   959 val _ = OuterSyntax.add_keywords
   960  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   961   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   962   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   963   "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   964   "constrains", "defines", "fixes", "for", "identifier", "if",
   965   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   966   "notes", "obtains", "open", "output", "overloaded", "shows",
   967   "structure", "unchecked", "uses", "where", "|"];
   968 
   969 val _ = OuterSyntax.add_parsers [
   970   (*theory structure*)
   971   theoryP, endP,
   972   (*markup commands*)
   973   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   974   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   975   (*theory sections*)
   976   classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
   977   nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
   978   no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
   979   constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
   980   theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
   981   ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
   982   simproc_setupP, parse_ast_translationP, parse_translationP,
   983   print_translationP, typed_print_translationP,
   984   print_ast_translationP, token_translationP, oracleP, contextP,
   985   localeP, classP, instanceP,
   986   (*proof commands*)
   987   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   988   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
   989   withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP,
   990   qedP, terminal_proofP, default_proofP, immediate_proofP,
   991   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
   992   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   993   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   994   interpretP,
   995   (*diagnostic commands*)
   996   pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
   997   print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
   998   print_theoremsP, print_localesP, print_localeP,
   999   print_registrationsP, print_attributesP, print_simpsetP,
  1000   print_rulesP, print_induct_rulesP, print_trans_rulesP,
  1001   print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
  1002   find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
  1003   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
  1004   print_termP, print_typeP,
  1005   (*system commands*)
  1006   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
  1007   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
  1008   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
  1009   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
  1010 
  1011 end;