src/Pure/Isar/isar_syn.ML
author haftmann
Sat Sep 15 19:27:44 2007 +0200 (2007-09-15 ago)
changeset 24589 d3fca349736c
parent 24451 7c205d006719
child 24624 b8383b1bbae3
permissions -rw-r--r--
clarified class interfaces and internals
     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 Sign.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 Class.axclass_cmd 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 (Sign.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 Sign.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 Sign.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 Sign.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 Sign.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 Sign.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 Sign.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 Sign.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_decl
   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
   393         >> (fn ((x, y), z) => Toplevel.print o
   394             Toplevel.theory_to_proof (Locale.interpretation I (apfst (pair true) 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
   402           Toplevel.proof' (Locale.interpret Seq.single (apfst (pair true) x) y z)));
   403 
   404 
   405 (* classes *)
   406 
   407 local
   408 
   409 val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
   410 val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
   411 
   412 in
   413 
   414 val classP =
   415   OuterSyntax.command "class" "define type class" K.thy_decl (
   416     P.name
   417     -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
   418     --| P.$$$ "=" -- (
   419       class_subP --| P.$$$ "+" -- class_bodyP
   420       || class_subP >> rpair []
   421       || class_bodyP >> pair [])
   422     -- P.opt_begin
   423     >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
   424         Toplevel.begin_local_theory begin
   425           (Class.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
   426 
   427 val instanceP =
   428   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
   429       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   430            >> Class.classrel_cmd
   431       || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
   432            >> Class.interpretation_in_class_cmd
   433       || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
   434            >> (fn (arities, defs) => Class.instance_cmd arities defs (fold (Code.add_func false)))
   435     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   436 
   437 val instantiationP =
   438   OuterSyntax.command "instantiation" "prove type arity" K.thy_decl (
   439       P.and_list1 P.arity -- P.opt_begin
   440            >> (fn (arities, begin) => (begin ? Toplevel.print)
   441             o Toplevel.begin_local_theory begin
   442                 (Instance.begin_instantiation_cmd arities)));
   443 
   444 val instance_proofP =
   445   OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
   446       (Scan.succeed ((Toplevel.print oo Toplevel.local_theory_to_proof NONE) Instance.proof_instantiation));
   447 
   448 end;
   449 
   450 
   451 (* code generation *)
   452 
   453 val code_datatypeP =
   454   OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
   455     (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
   456 
   457 
   458 
   459 (** proof commands **)
   460 
   461 (* statements *)
   462 
   463 fun gen_theorem kind =
   464   OuterSyntax.command kind ("state " ^ kind) K.thy_goal
   465     (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
   466       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
   467       SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
   468       (Toplevel.print o
   469        Toplevel.local_theory_to_proof' loc
   470          (Specification.theorem kind NONE (K I) a elems concl))));
   471 
   472 val theoremP = gen_theorem Thm.theoremK;
   473 val lemmaP = gen_theorem Thm.lemmaK;
   474 val corollaryP = gen_theorem Thm.corollaryK;
   475 
   476 val haveP =
   477   OuterSyntax.command "have" "state local goal"
   478     (K.tag_proof K.prf_goal)
   479     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   480 
   481 val henceP =
   482   OuterSyntax.command "hence" "abbreviates \"then have\""
   483     (K.tag_proof K.prf_goal)
   484     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   485 
   486 val showP =
   487   OuterSyntax.command "show" "state local goal, solving current obligation"
   488     (K.tag_proof K.prf_asm_goal)
   489     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   490 
   491 val thusP =
   492   OuterSyntax.command "thus" "abbreviates \"then show\""
   493     (K.tag_proof K.prf_asm_goal)
   494     (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   495 
   496 
   497 (* facts *)
   498 
   499 val facts = P.and_list1 SpecParse.xthms1;
   500 
   501 val thenP =
   502   OuterSyntax.command "then" "forward chaining"
   503     (K.tag_proof K.prf_chain)
   504     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
   505 
   506 val fromP =
   507   OuterSyntax.command "from" "forward chaining from given facts"
   508     (K.tag_proof K.prf_chain)
   509     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss)));
   510 
   511 val withP =
   512   OuterSyntax.command "with" "forward chaining from given and current facts"
   513     (K.tag_proof K.prf_chain)
   514     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss)));
   515 
   516 val noteP =
   517   OuterSyntax.command "note" "define facts"
   518     (K.tag_proof K.prf_decl)
   519     (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
   520 
   521 val usingP =
   522   OuterSyntax.command "using" "augment goal facts"
   523     (K.tag_proof K.prf_decl)
   524     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using)));
   525 
   526 val unfoldingP =
   527   OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
   528     (K.tag_proof K.prf_decl)
   529     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding)));
   530 
   531 
   532 (* proof context *)
   533 
   534 val fixP =
   535   OuterSyntax.command "fix" "fix local variables (Skolem constants)"
   536     (K.tag_proof K.prf_asm)
   537     (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
   538 
   539 val assumeP =
   540   OuterSyntax.command "assume" "assume propositions"
   541     (K.tag_proof K.prf_asm)
   542     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
   543 
   544 val presumeP =
   545   OuterSyntax.command "presume" "assume propositions, to be established later"
   546     (K.tag_proof K.prf_asm)
   547     (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
   548 
   549 val defP =
   550   OuterSyntax.command "def" "local definition"
   551     (K.tag_proof K.prf_asm)
   552     (P.and_list1
   553       (SpecParse.opt_thm_name ":" --
   554         ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   555     >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
   556 
   557 val obtainP =
   558   OuterSyntax.command "obtain" "generalized existence"
   559     (K.tag_proof K.prf_asm_goal)
   560     (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
   561       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
   562 
   563 val guessP =
   564   OuterSyntax.command "guess" "wild guessing (unstructured)"
   565     (K.tag_proof K.prf_asm_goal)
   566     (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
   567 
   568 val letP =
   569   OuterSyntax.command "let" "bind text variables"
   570     (K.tag_proof K.prf_decl)
   571     (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
   572       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind)));
   573 
   574 val case_spec =
   575   (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   576     P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
   577 
   578 val caseP =
   579   OuterSyntax.command "case" "invoke local context"
   580     (K.tag_proof K.prf_asm)
   581     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case)));
   582 
   583 
   584 (* proof structure *)
   585 
   586 val begin_blockP =
   587   OuterSyntax.command "{" "begin explicit proof block"
   588     (K.tag_proof K.prf_open)
   589     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
   590 
   591 val end_blockP =
   592   OuterSyntax.command "}" "end explicit proof block"
   593     (K.tag_proof K.prf_close)
   594     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
   595 
   596 val nextP =
   597   OuterSyntax.command "next" "enter next proof block"
   598     (K.tag_proof K.prf_block)
   599     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
   600 
   601 
   602 (* end proof *)
   603 
   604 val qedP =
   605   OuterSyntax.command "qed" "conclude (sub-)proof"
   606     (K.tag_proof K.qed_block)
   607     (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed));
   608 
   609 val terminal_proofP =
   610   OuterSyntax.command "by" "terminal backward proof"
   611     (K.tag_proof K.qed)
   612     (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof));
   613 
   614 val default_proofP =
   615   OuterSyntax.command ".." "default proof"
   616     (K.tag_proof K.qed)
   617     (Scan.succeed (Toplevel.print3 o IsarCmd.default_proof));
   618 
   619 val immediate_proofP =
   620   OuterSyntax.command "." "immediate proof"
   621     (K.tag_proof K.qed)
   622     (Scan.succeed (Toplevel.print3 o IsarCmd.immediate_proof));
   623 
   624 val done_proofP =
   625   OuterSyntax.command "done" "done proof"
   626     (K.tag_proof K.qed)
   627     (Scan.succeed (Toplevel.print3 o IsarCmd.done_proof));
   628 
   629 val skip_proofP =
   630   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
   631     (K.tag_proof K.qed)
   632     (Scan.succeed (Toplevel.print3 o IsarCmd.skip_proof));
   633 
   634 val forget_proofP =
   635   OuterSyntax.command "oops" "forget proof"
   636     (K.tag_proof K.qed_global)
   637     (Scan.succeed Toplevel.forget_proof);
   638 
   639 
   640 (* proof steps *)
   641 
   642 val deferP =
   643   OuterSyntax.command "defer" "shuffle internal proof state"
   644     (K.tag_proof K.prf_script)
   645     (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
   646 
   647 val preferP =
   648   OuterSyntax.command "prefer" "shuffle internal proof state"
   649     (K.tag_proof K.prf_script)
   650     (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
   651 
   652 val applyP =
   653   OuterSyntax.command "apply" "initial refinement step (unstructured)"
   654     (K.tag_proof K.prf_script)
   655     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
   656 
   657 val apply_endP =
   658   OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
   659     (K.tag_proof K.prf_script)
   660     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
   661 
   662 val proofP =
   663   OuterSyntax.command "proof" "backward proof"
   664     (K.tag_proof K.prf_block)
   665     (Scan.option Method.parse >> (fn m => Toplevel.print o
   666       Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o
   667       Toplevel.skip_proof (History.apply (fn i => i + 1))));
   668 
   669 
   670 (* calculational proof commands *)
   671 
   672 val calc_args =
   673   Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
   674 
   675 val alsoP =
   676   OuterSyntax.command "also" "combine calculation and current facts"
   677     (K.tag_proof K.prf_decl)
   678     (calc_args >> (Toplevel.proofs' o Calculation.also));
   679 
   680 val finallyP =
   681   OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
   682     (K.tag_proof K.prf_chain)
   683     (calc_args >> (Toplevel.proofs' o Calculation.finally_));
   684 
   685 val moreoverP =
   686   OuterSyntax.command "moreover" "augment calculation by current facts"
   687     (K.tag_proof K.prf_decl)
   688     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   689 
   690 val ultimatelyP =
   691   OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
   692     (K.tag_proof K.prf_chain)
   693     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
   694 
   695 
   696 (* proof navigation *)
   697 
   698 val backP =
   699   OuterSyntax.command "back" "backtracking of proof command"
   700     (K.tag_proof K.prf_script)
   701     (Scan.succeed (Toplevel.print o IsarCmd.back));
   702 
   703 
   704 (* history *)
   705 
   706 val cannot_undoP =
   707   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   708     (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
   709 
   710 val redoP =
   711   OuterSyntax.improper_command "redo" "redo last command" K.control
   712     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
   713 
   714 val undos_proofP =
   715   OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
   716     (P.nat >> ((Toplevel.no_timing o Toplevel.print) oo IsarCmd.undos_proof));
   717 
   718 val undoP =
   719   OuterSyntax.improper_command "undo" "undo last command" K.control
   720     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo));
   721 
   722 val killP =
   723   OuterSyntax.improper_command "kill" "kill current history node" K.control
   724     (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.kill));
   725 
   726 
   727 
   728 (** diagnostic commands (for interactive mode only) **)
   729 
   730 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   731 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
   732 
   733 val pretty_setmarginP =
   734   OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
   735     K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   736 
   737 val helpP =
   738   OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
   739     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   740 
   741 val print_commandsP =
   742   OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
   743     (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
   744 
   745 val print_configsP =
   746   OuterSyntax.improper_command "print_configs" "print configuration options" K.diag
   747     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
   748 
   749 val print_contextP =
   750   OuterSyntax.improper_command "print_context" "print theory context name" K.diag
   751     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
   752 
   753 val print_theoryP =
   754   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   755     (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
   756 
   757 val print_syntaxP =
   758   OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
   759     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
   760 
   761 val print_abbrevsP =
   762   OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
   763     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
   764 
   765 val print_theoremsP =
   766   OuterSyntax.improper_command "print_theorems"
   767       "print theorems of local theory or proof context" K.diag
   768     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
   769 
   770 val print_localesP =
   771   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
   772     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
   773 
   774 val print_classesP =
   775   OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
   776     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
   777       o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
   778 
   779 val print_localeP =
   780   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
   781     (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
   782 
   783 val print_registrationsP =
   784   OuterSyntax.improper_command "print_interps"
   785     "print interpretations of named locale" K.diag
   786     (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
   787       >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
   788 
   789 val print_attributesP =
   790   OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
   791     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
   792 
   793 val print_simpsetP =
   794   OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
   795     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
   796 
   797 val print_rulesP =
   798   OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
   799     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
   800 
   801 val print_induct_rulesP =
   802   OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules" K.diag
   803     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_induct_rules));
   804 
   805 val print_trans_rulesP =
   806   OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
   807     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
   808 
   809 val print_methodsP =
   810   OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag
   811     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
   812 
   813 val print_antiquotationsP =
   814   OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
   815     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   816 
   817 val thy_depsP =
   818   OuterSyntax.improper_command "thy_deps" "visualize theory dependencies"
   819     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
   820 
   821 val class_depsP =
   822   OuterSyntax.improper_command "class_deps" "visualize class dependencies"
   823     K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
   824 
   825 val thm_depsP =
   826   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   827     K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   828 
   829 local
   830 
   831 val criterion =
   832   P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
   833   P.reserved "intro" >> K FindTheorems.Intro ||
   834   P.reserved "elim" >> K FindTheorems.Elim ||
   835   P.reserved "dest" >> K FindTheorems.Dest ||
   836   P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> FindTheorems.Simp ||
   837   P.term >> FindTheorems.Pattern;
   838 
   839 val options =
   840   Scan.optional
   841     (P.$$$ "(" |--
   842       P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
   843         --| P.$$$ ")")) (NONE, true);
   844 in
   845 
   846 val find_theoremsP =
   847   OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
   848     (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
   849       >> (Toplevel.no_timing oo IsarCmd.find_theorems));
   850 
   851 end;
   852 
   853 val print_bindsP =
   854   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   855     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   856 
   857 val print_factsP =
   858   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
   859     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
   860 
   861 val print_casesP =
   862   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
   863     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
   864 
   865 val print_stmtsP =
   866   OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
   867     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   868 
   869 val print_thmsP =
   870   OuterSyntax.improper_command "thm" "print theorems" K.diag
   871     (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   872 
   873 val print_prfsP =
   874   OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
   875     (opt_modes -- Scan.option SpecParse.xthms1
   876       >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   877 
   878 val print_full_prfsP =
   879   OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
   880     (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   881 
   882 val print_propP =
   883   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   884     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
   885 
   886 val print_termP =
   887   OuterSyntax.improper_command "term" "read and print term" K.diag
   888     (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
   889 
   890 val print_typeP =
   891   OuterSyntax.improper_command "typ" "read and print type" K.diag
   892     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   893 
   894 val print_codesetupP =
   895   OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
   896     (Scan.succeed
   897       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
   898         (Code.print_codesetup o Toplevel.theory_of)));
   899 
   900 
   901 (** system commands (for interactive mode only) **)
   902 
   903 val cdP =
   904   OuterSyntax.improper_command "cd" "change current working directory" K.diag
   905     (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
   906 
   907 val pwdP =
   908   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   909     (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
   910 
   911 val use_thyP =
   912   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   913     (P.name >> (Toplevel.no_timing oo IsarCmd.use_thy));
   914 
   915 val touch_thyP =
   916   OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
   917     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
   918 
   919 val touch_child_thysP =
   920   OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
   921     (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
   922 
   923 val remove_thyP =
   924   OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
   925     (P.name >> (Toplevel.no_timing oo IsarCmd.remove_thy));
   926 
   927 val kill_thyP =
   928   OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   929     K.diag (P.name >> (Toplevel.no_timing oo IsarCmd.kill_thy));
   930 
   931 val display_draftsP =
   932   OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
   933     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
   934 
   935 val print_draftsP =
   936   OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
   937     K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
   938 
   939 val opt_limits =
   940   Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
   941 
   942 val prP =
   943   OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
   944     (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
   945 
   946 val disable_prP =
   947   OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
   948     (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
   949 
   950 val enable_prP =
   951   OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
   952     (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
   953 
   954 val commitP =
   955   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   956     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.use_commit));
   957 
   958 val quitP =
   959   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   960     (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
   961 
   962 val exitP =
   963   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   964     (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
   965 
   966 val init_toplevelP =
   967   OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
   968     (Scan.succeed (Toplevel.no_timing o IsarCmd.init_toplevel));
   969 
   970 val welcomeP =
   971   OuterSyntax.improper_command "welcome" "print welcome message" K.diag
   972     (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
   973 
   974 
   975 
   976 (** the Pure outer syntax **)
   977 
   978 (*keep keywords consistent with the parsers, otherwise be prepared for
   979   unexpected errors*)
   980 
   981 val _ = OuterSyntax.add_keywords
   982  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   983   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   984   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
   985   "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   986   "constrains", "defines", "fixes", "for", "identifier", "if",
   987   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   988   "notes", "obtains", "open", "output", "overloaded", "shows",
   989   "structure", "unchecked", "uses", "where", "|"];
   990 
   991 val _ = OuterSyntax.add_parsers [
   992   (*theory structure*)
   993   theoryP, endP,
   994   (*markup commands*)
   995   headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
   996   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   997   (*theory sections*)
   998   classesP, classrelP, defaultsortP, axclassP, typedeclP, typeabbrP,
   999   nontermP, aritiesP, judgmentP, constsP, finalconstsP, syntaxP,
  1000   no_syntaxP, translationsP, no_translationsP, axiomsP, defsP,
  1001   constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
  1002   theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
  1003   ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
  1004   simproc_setupP, parse_ast_translationP, parse_translationP,
  1005   print_translationP, typed_print_translationP,
  1006   print_ast_translationP, token_translationP, oracleP, contextP,
  1007   localeP, classP, instanceP, instantiationP, instance_proofP, code_datatypeP,
  1008   (*proof commands*)
  1009   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
  1010   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
  1011   withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP,
  1012   qedP, terminal_proofP, default_proofP, immediate_proofP,
  1013   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
  1014   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
  1015   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
  1016   interpretP,
  1017   (*diagnostic commands*)
  1018   pretty_setmarginP, helpP, print_classesP, print_commandsP,
  1019   print_configsP, print_contextP, print_theoryP, print_syntaxP,
  1020   print_abbrevsP, print_factsP, print_theoremsP, print_localesP,
  1021   print_localeP, print_registrationsP, print_attributesP,
  1022   print_simpsetP, print_rulesP, print_induct_rulesP,
  1023   print_trans_rulesP, print_methodsP, print_antiquotationsP,
  1024   thy_depsP, class_depsP, thm_depsP, find_theoremsP, print_bindsP,
  1025   print_casesP, print_stmtsP, print_thmsP, print_prfsP,
  1026   print_full_prfsP, print_propP, print_termP, print_typeP,
  1027   print_codesetupP,
  1028   (*system commands*)
  1029   cdP, pwdP, use_thyP, touch_thyP, touch_child_thysP, remove_thyP,
  1030   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
  1031   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
  1032 
  1033 end;