src/Pure/Isar/isar_syn.ML
author kleing
Tue Mar 06 05:31:23 2007 +0100 (2007-03-06 ago)
changeset 22415 c310ca7cd47f
parent 22385 cc2be3315e72
child 22417 014e7696ac6b
permissions -rw-r--r--
find_theorems: moved with_dup into the brackets, i.e.

find_theorems (20 with_dups) "some term" ..
     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.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    92       >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
    93 
    94 
    95 (* types *)
    96 
    97 val typedeclP =
    98   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
    99     (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
   100       Toplevel.theory (Theory.add_typedecls [(a, args, mx)])));
   101 
   102 val typeabbrP =
   103   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   104     (Scan.repeat1
   105       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')))
   106       >> (Toplevel.theory o Theory.add_tyabbrs o
   107         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   108 
   109 val nontermP =
   110   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   111     K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
   112 
   113 val aritiesP =
   114   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   115     (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
   116 
   117 
   118 (* consts and syntax *)
   119 
   120 val judgmentP =
   121   OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
   122     (P.const >> (Toplevel.theory o ObjectLogic.add_judgment));
   123 
   124 val constsP =
   125   OuterSyntax.command "consts" "declare constants" K.thy_decl
   126     (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
   127 
   128 val opt_overloaded = P.opt_keyword "overloaded";
   129 
   130 val finalconstsP =
   131   OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
   132     (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
   133 
   134 val mode_spec =
   135   (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
   136 
   137 val opt_mode =
   138   Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
   139 
   140 val syntaxP =
   141   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   142     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   143 
   144 val no_syntaxP =
   145   OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
   146     (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.del_modesyntax));
   147 
   148 
   149 (* translations *)
   150 
   151 val trans_pat =
   152   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   153 
   154 fun trans_arrow toks =
   155   ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
   156     (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
   157     (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
   158 
   159 val trans_line =
   160   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   161     >> (fn (left, (arr, right)) => arr (left, right));
   162 
   163 val translationsP =
   164   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   165     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   166 
   167 val no_translationsP =
   168   OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
   169     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.del_trrules));
   170 
   171 
   172 (* axioms and definitions *)
   173 
   174 val axiomsP =
   175   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   176     (Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
   177 
   178 val opt_unchecked_overloaded =
   179   Scan.optional (P.$$$ "(" |-- P.!!!
   180     (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
   181       P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
   182 
   183 val defsP =
   184   OuterSyntax.command "defs" "define constants" K.thy_decl
   185     (opt_unchecked_overloaded -- Scan.repeat1 SpecParse.spec_name
   186       >> (Toplevel.theory o IsarCmd.add_defs));
   187 
   188 
   189 (* old constdefs *)
   190 
   191 val old_constdecl =
   192   P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
   193   P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
   194     --| Scan.option P.where_ >> P.triple1 ||
   195   P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
   196 
   197 val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   198 
   199 val structs =
   200   Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
   201 
   202 val constdefsP =
   203   OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
   204     (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
   205 
   206 
   207 (* constant definitions and abbreviations *)
   208 
   209 val constdecl =
   210   P.name --
   211     (P.where_ >> K (NONE, NoSyn) ||
   212       P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
   213       Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
   214   >> P.triple2;
   215 
   216 val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   217 
   218 val definitionP =
   219   OuterSyntax.command "definition" "constant definition" K.thy_decl
   220     (P.opt_target -- constdef
   221     >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
   222 
   223 val abbreviationP =
   224   OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
   225     (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
   226     >> (fn ((loc, mode), args) =>
   227         Toplevel.local_theory loc (Specification.abbreviation mode args)));
   228 
   229 val notationP =
   230   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
   231     (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   232     >> (fn ((loc, mode), args) =>
   233         Toplevel.local_theory loc (Specification.notation mode args)));
   234 
   235 
   236 (* constant specifications *)
   237 
   238 val axiomatizationP =
   239   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
   240     (P.opt_target --
   241      (Scan.optional P.fixes [] --
   242       Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
   243     >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
   244 
   245 
   246 (* theorems *)
   247 
   248 fun theorems kind = P.opt_target -- SpecParse.name_facts
   249   >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
   250 
   251 val theoremsP =
   252   OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
   253 
   254 val lemmasP =
   255   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
   256 
   257 val declareP =
   258   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
   259     (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
   260       >> (fn (loc, args) => Toplevel.local_theory loc
   261           (#2 o Specification.theorems "" [(("", []), args)])));
   262 
   263 
   264 (* name space entry path *)
   265 
   266 val globalP =
   267   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   268     (Scan.succeed (Toplevel.theory Sign.root_path));
   269 
   270 val localP =
   271   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   272     (Scan.succeed (Toplevel.theory Sign.local_path));
   273 
   274 val hideP =
   275   OuterSyntax.command "hide" "hide names from given name space" K.thy_decl
   276     ((P.opt_keyword "open" >> not) -- (P.name -- Scan.repeat1 P.xname) >>
   277       (Toplevel.theory o uncurry Sign.hide_names));
   278 
   279 
   280 (* use ML text *)
   281 
   282 val useP =
   283   OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag)
   284     (P.path >> (Toplevel.no_timing oo IsarCmd.use));
   285 
   286 val mlP =
   287   OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
   288     (P.text >> IsarCmd.use_mltext true);
   289 
   290 val ml_commandP =
   291   OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
   292     (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
   293 
   294 val ml_setupP =
   295   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
   296     (P.text >> IsarCmd.use_mltext_theory);
   297 
   298 val setupP =
   299   OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
   300     (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup));
   301 
   302 val method_setupP =
   303   OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
   304     (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
   305       >> (Toplevel.theory o Method.method_setup));
   306 
   307 val declarationP =
   308   OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
   309     (P.opt_target -- P.text
   310     >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
   311 
   312 val simproc_setupP =
   313   OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
   314     (P.opt_target --
   315       P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
   316       Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
   317     >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
   318 
   319 
   320 (* translation functions *)
   321 
   322 val trfun = P.opt_keyword "advanced" -- P.text;
   323 
   324 val parse_ast_translationP =
   325   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   326     (K.tag_ml K.thy_decl)
   327     (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
   328 
   329 val parse_translationP =
   330   OuterSyntax.command "parse_translation" "install parse translation functions"
   331     (K.tag_ml K.thy_decl)
   332     (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
   333 
   334 val print_translationP =
   335   OuterSyntax.command "print_translation" "install print translation functions"
   336     (K.tag_ml K.thy_decl)
   337     (trfun >> (Toplevel.theory o IsarCmd.print_translation));
   338 
   339 val typed_print_translationP =
   340   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   341     (K.tag_ml K.thy_decl)
   342     (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
   343 
   344 val print_ast_translationP =
   345   OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   346     (K.tag_ml K.thy_decl)
   347     (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
   348 
   349 val token_translationP =
   350   OuterSyntax.command "token_translation" "install token translation functions"
   351     (K.tag_ml K.thy_decl)
   352     (P.text >> (Toplevel.theory o IsarCmd.token_translation));
   353 
   354 
   355 (* oracles *)
   356 
   357 val oracleP =
   358   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
   359     (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
   360       -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
   361 
   362 
   363 (* local theories *)
   364 
   365 val contextP =
   366   OuterSyntax.command "context" "enter local theory context" K.thy_decl
   367     (P.name --| P.begin >> (fn name =>
   368       Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
   369 
   370 
   371 (* locales *)
   372 
   373 val locale_val =
   374   (SpecParse.locale_expr --
   375     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   376   Scan.repeat1 SpecParse.context_element >> pair Locale.empty);
   377 
   378 val localeP =
   379   OuterSyntax.command "locale" "define named proof context" K.thy_decl
   380     ((P.opt_keyword "open" >> (fn true => NONE | false => SOME "")) -- P.name
   381         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
   382         -- P.opt_begin
   383       >> (fn (((is_open, name), (expr, elems)), begin) =>
   384           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   385             (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
   386 
   387 val interpretationP =
   388   OuterSyntax.command "interpretation"
   389     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
   390     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
   391       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
   392       SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts >> (fn ((x, y), z) =>
   393         Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) x) y z)));
   394 
   395 val interpretP =
   396   OuterSyntax.command "interpret"
   397     "prove and register interpretation of locale expression in proof context"
   398     (K.tag_proof K.prf_goal)
   399     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   400       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
   401 
   402 
   403 (* classes *)
   404 
   405 local
   406 
   407 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
   408 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
   409 
   410 in
   411 
   412 val classP =
   413   OuterSyntax.command "class" "define type class" K.thy_decl (
   414     P.name
   415     -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
   416     --| P.$$$ "=" -- (
   417       class_subP --| P.$$$ "+" -- class_bodyP
   418       || class_subP >> rpair []
   419       || class_bodyP >> pair [])
   420     -- P.opt_begin
   421     >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
   422         Toplevel.begin_local_theory begin
   423           (ClassPackage.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
   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.optional (P.$$$ "(" |-- P.!!!
   813                         (Scan.option P.nat --
   814                          Scan.optional (P.reserved "with_dups" >> K false) true
   815                          --| P.$$$ ")")) (NONE, false) --
   816      Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   817       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
   818 
   819 val print_bindsP =
   820   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   821     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   822 
   823 val print_factsP =
   824   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
   825     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
   826 
   827 val print_casesP =
   828   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
   829     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
   830 
   831 val print_stmtsP =
   832   OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
   833     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   834 
   835 val print_thmsP =
   836   OuterSyntax.improper_command "thm" "print theorems" K.diag
   837     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   838 
   839 val print_prfsP =
   840   OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
   841     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   842 
   843 val print_full_prfsP =
   844   OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
   845     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   846 
   847 val print_propP =
   848   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   849     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
   850 
   851 val print_termP =
   852   OuterSyntax.improper_command "term" "read and print term" K.diag
   853     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
   854 
   855 val print_typeP =
   856   OuterSyntax.improper_command "typ" "read and print type" K.diag
   857     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   858 
   859 
   860 
   861 (** system commands (for interactive mode only) **)
   862 
   863 val cdP =
   864   OuterSyntax.improper_command "cd" "change current working directory" K.diag
   865     (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
   866 
   867 val pwdP =
   868   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   869     (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
   870 
   871 val use_thyP =
   872   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   873     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
   874 
   875 val use_thy_onlyP =
   876   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
   877     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy_only));
   878 
   879 val update_thyP =
   880   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   881     (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy));
   882 
   883 val update_thy_onlyP =
   884   OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
   885     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.update_thy_only));
   886 
   887 val touch_thyP =
   888   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
   889     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
   890 
   891 val touch_all_thysP =
   892   OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
   893     (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
   894 
   895 val touch_child_thysP =
   896   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
   897     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
   898 
   899 val remove_thyP =
   900   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   901     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   902 
   903 val kill_thyP =
   904   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   905     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
   906 
   907 val display_draftsP =
   908   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
   909     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
   910 
   911 val print_draftsP =
   912   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
   913     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
   914 
   915 val opt_limits =
   916   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   917 
   918 val prP =
   919   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
   920     (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
   921 
   922 val disable_prP =
   923   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
   924     (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
   925 
   926 val enable_prP =
   927   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   928     (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
   929 
   930 val commitP =
   931   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   932     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
   933 
   934 val quitP =
   935   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   936     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
   937 
   938 val exitP =
   939   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   940     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
   941 
   942 val init_toplevelP =
   943   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
   944     (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel));
   945 
   946 val welcomeP =
   947   OuterSyntax.improper_command "welcome" "print welcome message" K.diag
   948     (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
   949 
   950 
   951 
   952 (** the Pure outer syntax **)
   953 
   954 (*keep keywords consistent with the parsers, including those in
   955   outer_parse.ML, otherwise be prepared for unexpected errors*)
   956 
   957 val _ = OuterSyntax.add_keywords
   958  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   959   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   960   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   961   "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   962   "constrains", "defines", "fixes", "for", "identifier", "if",
   963   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   964   "notes", "obtains", "open", "output", "overloaded", "shows",
   965   "structure", "unchecked", "uses", "where", "|"];
   966 
   967 val _ = OuterSyntax.add_parsers [
   968   (*theory structure*)
   969   theoryP, endP,
   970   (*markup commands*)
   971   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   972   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   973   (*theory sections*)
   974   classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
   975   nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
   976   no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
   977   constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
   978   theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
   979   ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
   980   simproc_setupP, parse_ast_translationP, parse_translationP,
   981   print_translationP, typed_print_translationP,
   982   print_ast_translationP, token_translationP, oracleP, contextP,
   983   localeP, classP, instanceP,
   984   (*proof commands*)
   985   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   986   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
   987   withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP,
   988   qedP, terminal_proofP, default_proofP, immediate_proofP,
   989   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
   990   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   991   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   992   interpretP,
   993   (*diagnostic commands*)
   994   pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
   995   print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
   996   print_theoremsP, print_localesP, print_localeP,
   997   print_registrationsP, print_attributesP, print_simpsetP,
   998   print_rulesP, print_induct_rulesP, print_trans_rulesP,
   999   print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
  1000   find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
  1001   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
  1002   print_termP, print_typeP,
  1003   (*system commands*)
  1004   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
  1005   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
  1006   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
  1007   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
  1008 
  1009 end;