src/Pure/Isar/isar_syn.ML
author wenzelm
Wed May 26 22:44:41 1999 +0200 (1999-05-26 ago)
changeset 6735 e5138b3dbd3b
parent 6727 c8dba1da73cc
child 6742 6b5cb872d997
permissions -rw-r--r--
cannot_undo;
qed_block keywords;
     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 signature ISAR_SYN =
     9 sig
    10   val keywords: string list
    11   val parsers: OuterSyntax.parser list
    12 end;
    13 
    14 structure IsarSyn: ISAR_SYN =
    15 struct
    16 
    17 structure P = OuterParse and K = OuterSyntax.Keyword;
    18 
    19 
    20 (** init and exit **)
    21 
    22 val theoryP =
    23   OuterSyntax.command "theory" "begin theory" K.thy_begin
    24     (OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
    25 
    26 val end_excursionP =
    27   OuterSyntax.command "end" "end current excursion" K.thy_end
    28     (Scan.succeed (Toplevel.print o Toplevel.exit));
    29 
    30 val kill_excursionP =
    31   OuterSyntax.command "kill" "kill current excursion" K.control
    32     (Scan.succeed (Toplevel.print o Toplevel.kill));
    33 
    34 val contextP =
    35   OuterSyntax.improper_command "context" "switch theory context" K.thy_begin
    36     (P.name >> (Toplevel.print oo IsarThy.context));
    37 
    38 val update_contextP =
    39   OuterSyntax.improper_command "update_context" "switch theory context, forcing update" K.thy_begin
    40     (P.name >> (Toplevel.print oo IsarThy.update_context));
    41 
    42 
    43 
    44 (** theory sections **)
    45 
    46 (* formal comments *)
    47 
    48 val textP = OuterSyntax.command "text" "formal comments" K.thy_decl
    49   (P.comment >> (Toplevel.theory o IsarThy.add_text));
    50 
    51 val titleP = OuterSyntax.command "title" "document title" K.thy_heading
    52   ((P.comment -- Scan.optional P.comment Comment.none -- Scan.optional P.comment Comment.none)
    53     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    54 
    55 val chapterP = OuterSyntax.command "chapter" "chapter heading" K.thy_heading
    56   (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
    57 
    58 val sectionP = OuterSyntax.command "section" "section heading" K.thy_heading
    59   (P.comment >> (Toplevel.theory o IsarThy.add_section));
    60 
    61 val subsectionP = OuterSyntax.command "subsection" "subsection heading" K.thy_heading
    62   (P.comment >> (Toplevel.theory o IsarThy.add_subsection));
    63 
    64 val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading" K.thy_heading
    65   (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    66 
    67 
    68 (* classes and sorts *)
    69 
    70 val classesP =
    71   OuterSyntax.command "classes" "declare type classes" K.thy_decl
    72     (Scan.repeat1 (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [])
    73       -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes));
    74 
    75 val classrelP =
    76   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    77     (P.xname -- (P.$$$ "<" |-- P.!!! P.xname) -- P.marg_comment
    78       >> (Toplevel.theory o IsarThy.add_classrel));
    79 
    80 val defaultsortP =
    81   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    82     (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort));
    83 
    84 
    85 (* types *)
    86 
    87 val typedeclP =
    88   OuterSyntax.command "typedecl" "Pure type declaration" K.thy_decl
    89     (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) =>
    90       Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt))));
    91 
    92 val typeabbrP =
    93   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
    94     (Scan.repeat1
    95       (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)) -- P.marg_comment)
    96       >> (Toplevel.theory o IsarThy.add_tyabbrs o
    97         map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt))));
    98 
    99 val nontermP =
   100   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   101     K.thy_decl (Scan.repeat1 (P.name -- P.marg_comment)
   102       >> (Toplevel.theory o IsarThy.add_nonterminals));
   103 
   104 val aritiesP =
   105   OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   106     (Scan.repeat1 ((P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) -- P.marg_comment)
   107       >> (Toplevel.theory o IsarThy.add_arities));
   108 
   109 
   110 (* consts and syntax *)
   111 
   112 val constsP =
   113   OuterSyntax.command "consts" "declare constants" K.thy_decl
   114     (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
   115 
   116 val opt_mode =
   117   Scan.optional
   118     (P.$$$ "(" |-- P.!!! (P.name -- Scan.optional (P.$$$ "output" >> K false) true --| P.$$$ ")"))
   119     ("", true);
   120 
   121 val syntaxP =
   122   OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   123     (opt_mode -- Scan.repeat1 (P.const -- P.marg_comment)
   124       >> (Toplevel.theory o uncurry IsarThy.add_modesyntax));
   125 
   126 
   127 (* translations *)
   128 
   129 val trans_pat =
   130   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   131 
   132 fun trans_arrow toks =
   133   (P.$$$ "=>" >> K Syntax.ParseRule ||
   134     P.$$$ "<=" >> K Syntax.PrintRule ||
   135     P.$$$ "==" >> K Syntax.ParsePrintRule) toks;
   136 
   137 val trans_line =
   138   trans_pat -- P.!!! (trans_arrow -- trans_pat)
   139     >> (fn (left, (arr, right)) => arr (left, right));
   140 
   141 val translationsP =
   142   OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   143     (Scan.repeat1 (trans_line -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_trrules));
   144 
   145 
   146 (* axioms and definitions *)
   147 
   148 val axiomsP =
   149   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   150     (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms));
   151 
   152 val defsP =
   153   OuterSyntax.command "defs" "define constants" K.thy_decl
   154     (Scan.repeat1 (P.spec_opt_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_defs));
   155 
   156 val constdefsP =
   157   OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
   158     (Scan.repeat1 ((P.const -- P.marg_comment) -- (P.term -- P.marg_comment))
   159       >> (Toplevel.theory o IsarThy.add_constdefs));
   160 
   161 
   162 (* theorems *)
   163 
   164 val facts = P.opt_thm_name "=" -- P.xthms1;
   165 
   166 val theoremsP =
   167   OuterSyntax.command "theorems" "define theorems" K.thy_decl
   168     (facts -- P.marg_comment >> (Toplevel.theory o IsarThy.have_theorems));
   169 
   170 val lemmasP =
   171   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   172     (facts -- P.marg_comment >> (Toplevel.theory o IsarThy.have_lemmas));
   173 
   174 
   175 (* name space entry path *)
   176 
   177 val globalP =
   178   OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   179     (Scan.succeed (Toplevel.theory PureThy.global_path));
   180 
   181 val localP =
   182   OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   183     (Scan.succeed (Toplevel.theory PureThy.local_path));
   184 
   185 val pathP =
   186   OuterSyntax.command "path" "modify name-space entry path" K.thy_decl
   187     (P.xname >> (Toplevel.theory o Theory.add_path));
   188 
   189 
   190 (* use ML text *)
   191 
   192 val useP =
   193   OuterSyntax.command "use" "eval ML text from file" K.diag
   194     (P.name >> IsarCmd.use);
   195 
   196 val mlP =
   197   OuterSyntax.command "ML" "eval ML text" K.diag
   198     (P.text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   199 
   200 val setupP =
   201   OuterSyntax.command "setup" "apply ML theory transformer" K.thy_decl
   202     (P.text >> (Toplevel.theory o IsarThy.use_setup));
   203 
   204 
   205 (* translation functions *)
   206 
   207 val parse_ast_translationP =
   208   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
   209     (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   210 
   211 val parse_translationP =
   212   OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
   213     (P.text >> (Toplevel.theory o IsarThy.parse_translation));
   214 
   215 val print_translationP =
   216   OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
   217     (P.text >> (Toplevel.theory o IsarThy.print_translation));
   218 
   219 val typed_print_translationP =
   220   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   221     K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
   222 
   223 val print_ast_translationP =
   224   OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
   225     (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
   226 
   227 val token_translationP =
   228   OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
   229     (P.text >> (Toplevel.theory o IsarThy.token_translation));
   230 
   231 
   232 (* oracles *)
   233 
   234 val oracleP =
   235   OuterSyntax.command "oracle" "install oracle" K.thy_decl
   236     (P.name -- P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.add_oracle));
   237 
   238 
   239 
   240 (** proof commands **)
   241 
   242 (* statements *)
   243 
   244 val is_props = P.$$$ "(" |-- P.!!! (Scan.repeat1 (P.$$$ "is" |-- P.prop) --| P.$$$ ")");
   245 val propp = P.prop -- Scan.optional is_props [];
   246 fun statement f = (P.opt_thm_name ":" -- propp >> P.triple1) -- P.marg_comment >> f;
   247 
   248 val theoremP =
   249   OuterSyntax.command "theorem" "state theorem" K.thy_goal
   250     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   251 
   252 val lemmaP =
   253   OuterSyntax.command "lemma" "state lemma" K.thy_goal
   254     (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   255 
   256 val showP =
   257   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
   258     (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   259 
   260 val haveP =
   261   OuterSyntax.command "have" "state local goal" K.prf_goal
   262     (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   263 
   264 val thusP =
   265   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
   266     (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
   267 
   268 val henceP =
   269   OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
   270     (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
   271 
   272 
   273 (* facts *)
   274 
   275 val thenP =
   276   OuterSyntax.command "then" "forward chaining" K.prf_chain
   277     (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain)));
   278 
   279 val fromP =
   280   OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
   281     (P.xthms1 -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
   282 
   283 val factsP =
   284   OuterSyntax.command "note" "define facts" K.prf_decl
   285     (facts -- P.marg_comment >> (Toplevel.proof o IsarThy.have_facts));
   286 
   287 
   288 (* proof context *)
   289 
   290 val assumeP =
   291   OuterSyntax.command "assume" "assume propositions" K.prf_decl
   292     ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
   293       >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
   294 
   295 val fixP =
   296   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
   297     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
   298       >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
   299 
   300 val letP =
   301   OuterSyntax.command "let" "bind text variables" K.prf_decl
   302     (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
   303       >> (Toplevel.print oo (Toplevel.proof o IsarThy.match_bind)));
   304 
   305 
   306 (* proof structure *)
   307 
   308 val beginP =
   309   OuterSyntax.command "{{" "begin explicit proof block" K.prf_block
   310     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   311 
   312 val endP =
   313   OuterSyntax.command "}}" "end explicit proof block" K.prf_block
   314     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
   315 
   316 val nextP =
   317   OuterSyntax.command "next" "enter next proof block" K.prf_block
   318     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   319 
   320 
   321 (* end proof *)
   322 
   323 val kill_proofP =
   324   OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
   325     (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   326 
   327 val qed_withP =
   328   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
   329     K.qed_block
   330     (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
   331       >> (uncurry IsarThy.global_qed_with));
   332 
   333 val qedP =
   334   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
   335     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
   336 
   337 val terminal_proofP =
   338   OuterSyntax.command "by" "terminal backward proof" K.qed
   339     (P.method -- P.interest >> IsarThy.terminal_proof);
   340 
   341 val immediate_proofP =
   342   OuterSyntax.command "." "immediate proof" K.qed
   343     (Scan.succeed IsarThy.immediate_proof);
   344 
   345 val default_proofP =
   346   OuterSyntax.command ".." "default proof" K.qed
   347     (Scan.succeed IsarThy.default_proof);
   348 
   349 
   350 (* proof steps *)
   351 
   352 val refineP =
   353   OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
   354     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   355 
   356 val then_refineP =
   357   OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
   358     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   359 
   360 val proofP =
   361   OuterSyntax.command "proof" "backward proof" K.prf_block
   362     (P.interest -- Scan.option (P.method -- P.interest)
   363       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   364 
   365 
   366 (* proof history *)
   367 
   368 val cannot_undoP =
   369   OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
   370     (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
   371 
   372 val clear_undoP =
   373   OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
   374     (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
   375 
   376 val undoP =
   377   OuterSyntax.improper_command "undo" "undo last command" K.control
   378     (Scan.succeed (Toplevel.print o IsarCmd.undo));
   379 
   380 val redoP =
   381   OuterSyntax.improper_command "redo" "redo last command" K.control
   382     (Scan.succeed (Toplevel.print o IsarCmd.redo));
   383 
   384 val undosP =
   385   OuterSyntax.improper_command "undos" "undo last commands" K.control
   386     (P.nat >> (fn n => Toplevel.print o IsarCmd.undos n));
   387 
   388 val backP =
   389   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
   390     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   391 
   392 val prevP =
   393   OuterSyntax.improper_command "prev" "previous proof state" K.control
   394     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   395 
   396 val upP =
   397   OuterSyntax.improper_command "up" "upper proof state" K.control
   398     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   399 
   400 val topP =
   401   OuterSyntax.improper_command "top" "to initial proof state" K.control
   402     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   403 
   404 
   405 
   406 (** diagnostic commands (for interactive mode only) **)
   407 
   408 val print_commandsP =
   409   OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
   410     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   411 
   412 val print_theoryP =
   413   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   414     (Scan.succeed IsarCmd.print_theory);
   415 
   416 val print_syntaxP =
   417   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
   418     (Scan.succeed IsarCmd.print_syntax);
   419 
   420 val print_theoremsP =
   421   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag
   422     (Scan.succeed IsarCmd.print_theorems);
   423 
   424 val print_attributesP =
   425   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
   426     (Scan.succeed IsarCmd.print_attributes);
   427 
   428 val print_methodsP =
   429   OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
   430     (Scan.succeed IsarCmd.print_methods);
   431 
   432 val print_bindsP =
   433   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   434     (Scan.succeed IsarCmd.print_binds);
   435 
   436 val print_lthmsP =
   437   OuterSyntax.improper_command "print_facts" "print local theorems of proof context" K.diag
   438     (Scan.succeed IsarCmd.print_lthms);
   439 
   440 val print_thmsP =
   441   OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthm >> IsarCmd.print_thms);
   442 
   443 val print_propP =
   444   OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   445     (P.term >> IsarCmd.print_prop);
   446 
   447 val print_termP =
   448   OuterSyntax.improper_command "term" "read and print term" K.diag
   449     (P.term >> IsarCmd.print_term);
   450 
   451 val print_typeP =
   452   OuterSyntax.improper_command "typ" "read and print type" K.diag
   453     (P.typ >> IsarCmd.print_type);
   454 
   455 
   456 
   457 (** system commands (for interactive mode only) **)
   458 
   459 val cdP =
   460   OuterSyntax.improper_command "cd" "change current working directory" K.control
   461     (P.name >> IsarCmd.cd);
   462 
   463 val pwdP =
   464   OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   465     (Scan.succeed IsarCmd.pwd);
   466 
   467 val use_thyP =
   468   OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   469     (P.name >> IsarCmd.use_thy);
   470 
   471 val use_thy_onlyP =
   472   OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" K.diag
   473     (P.name >> IsarCmd.use_thy_only);
   474 
   475 val update_thyP =
   476   OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   477     (P.name >> IsarCmd.update_thy);
   478 
   479 val prP =
   480   OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   481     (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   482 
   483 
   484 val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
   485 
   486 val commitP =
   487   OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   488     (opt_unit >> (K IsarCmd.use_commit));
   489 
   490 val quitP =
   491   OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   492     (opt_unit >> (K IsarCmd.quit));
   493 
   494 val exitP =
   495   OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   496     (Scan.succeed IsarCmd.exit);
   497 
   498 val restartP =
   499   OuterSyntax.improper_command "restart" "restart Isar loop" K.control
   500     (Scan.succeed IsarCmd.restart);
   501 
   502 val breakP =
   503   OuterSyntax.improper_command "break" "discontinue excursion (keep current state)" K.control
   504     (Scan.succeed IsarCmd.break);
   505 
   506 
   507 
   508 (** the Pure outer syntax **)
   509 
   510 (*keep keywords consistent with the parsers, including those in
   511   outer_parse.ML, otherwise be prepared for unexpected errors*)
   512 
   513 val keywords =
   514  ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
   515   "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
   516   "infixl", "infixr", "is", "output", "{", "|", "}"];
   517 
   518 val parsers = [
   519   (*theory structure*)
   520   theoryP, end_excursionP, kill_excursionP, contextP, update_contextP,
   521   (*theory sections*)
   522   textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP,
   523   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   524   aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
   525   constdefsP, theoremsP, lemmasP, globalP, localP, pathP, useP, mlP,
   526   setupP, parse_ast_translationP, parse_translationP,
   527   print_translationP, typed_print_translationP,
   528   print_ast_translationP, token_translationP, oracleP,
   529   (*proof commands*)
   530   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
   531   thenP, fromP, factsP, beginP, endP, nextP, kill_proofP, qed_withP,
   532   qedP, terminal_proofP, immediate_proofP, default_proofP, refineP,
   533   then_refineP, proofP, cannot_undoP, clear_undoP, undoP, redoP,
   534   undosP, backP, prevP, upP, topP,
   535   (*diagnostic commands*)
   536   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   537   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   538   print_thmsP, print_propP, print_termP, print_typeP,
   539   (*system commands*)
   540   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
   541   quitP, exitP, restartP, breakP];
   542 
   543 
   544 end;
   545 
   546 
   547 (*install the Pure outer syntax*)
   548 OuterSyntax.add_keywords IsarSyn.keywords;
   549 OuterSyntax.add_parsers IsarSyn.parsers;