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