src/Pure/Pure.thy
author wenzelm
Thu Nov 08 13:42:36 2018 +0100 (7 months ago)
changeset 69262 f94726501b37
parent 69059 70f9826753f6
child 69349 7cef9e386ffe
permissions -rw-r--r--
more standard Resources.provide_parse_files: avoid duplicate markup reports;
     1 (*  Title:      Pure/Pure.thy
     2     Author:     Makarius
     3 
     4 The Pure theory, with definitions of Isar commands and some lemmas.
     5 *)
     6 
     7 theory Pure
     8 keywords
     9     "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    10     "\<subseteq>" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
    11     "overloaded" "pervasive" "premises" "structure" "unchecked"
    12   and "private" "qualified" :: before_command
    13   and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
    14     "obtains" "shows" "when" "where" "|" :: quasi_command
    15   and "text" "txt" :: document_body
    16   and "text_raw" :: document_raw
    17   and "default_sort" :: thy_decl
    18   and "typedecl" "type_synonym" "nonterminal" "judgment"
    19     "consts" "syntax" "no_syntax" "translations" "no_translations"
    20     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    21     "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
    22     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    23   and "external_file" "bibtex_file" :: thy_load
    24   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
    25   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    26   and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
    27   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    28   and "ML_val" "ML_command" :: diag % "ML"
    29   and "simproc_setup" :: thy_decl % "ML"
    30   and "setup" "local_setup" "attribute_setup" "method_setup"
    31     "declaration" "syntax_declaration"
    32     "parse_ast_translation" "parse_translation" "print_translation"
    33     "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
    34   and "bundle" :: thy_decl_block
    35   and "unbundle" :: thy_decl
    36   and "include" "including" :: prf_decl
    37   and "print_bundles" :: diag
    38   and "context" "locale" "experiment" :: thy_decl_block
    39   and "interpret" :: prf_goal % "proof"
    40   and "interpretation" "global_interpretation" "sublocale" :: thy_goal
    41   and "class" :: thy_decl_block
    42   and "subclass" :: thy_goal
    43   and "instantiation" :: thy_decl_block
    44   and "instance" :: thy_goal
    45   and "overloading" :: thy_decl_block
    46   and "code_datatype" :: thy_decl
    47   and "theorem" "lemma" "corollary" "proposition" :: thy_goal
    48   and "schematic_goal" :: thy_goal
    49   and "notepad" :: thy_decl_block
    50   and "have" :: prf_goal % "proof"
    51   and "hence" :: prf_goal % "proof"
    52   and "show" :: prf_asm_goal % "proof"
    53   and "thus" :: prf_asm_goal % "proof"
    54   and "then" "from" "with" :: prf_chain % "proof"
    55   and "note" :: prf_decl % "proof"
    56   and "supply" :: prf_script % "proof"
    57   and "using" "unfolding" :: prf_decl % "proof"
    58   and "fix" "assume" "presume" "define" :: prf_asm % "proof"
    59   and "consider" :: prf_goal % "proof"
    60   and "obtain" :: prf_asm_goal % "proof"
    61   and "guess" :: prf_script_asm_goal % "proof"
    62   and "let" "write" :: prf_decl % "proof"
    63   and "case" :: prf_asm % "proof"
    64   and "{" :: prf_open % "proof"
    65   and "}" :: prf_close % "proof"
    66   and "next" :: next_block % "proof"
    67   and "qed" :: qed_block % "proof"
    68   and "by" ".." "." "sorry" "\<proof>" :: "qed" % "proof"
    69   and "done" :: "qed_script" % "proof"
    70   and "oops" :: qed_global % "proof"
    71   and "defer" "prefer" "apply" :: prf_script % "proof"
    72   and "apply_end" :: prf_script % "proof"
    73   and "subgoal" :: prf_script_goal % "proof"
    74   and "proof" :: prf_block % "proof"
    75   and "also" "moreover" :: prf_decl % "proof"
    76   and "finally" "ultimately" :: prf_chain % "proof"
    77   and "back" :: prf_script % "proof"
    78   and "help" "print_commands" "print_options" "print_context" "print_theory"
    79     "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
    80     "print_theorems" "print_locales" "print_classes" "print_locale"
    81     "print_interps" "print_dependencies" "print_attributes"
    82     "print_simpset" "print_rules" "print_trans_rules" "print_methods"
    83     "print_antiquotations" "print_ML_antiquotations" "thy_deps"
    84     "locale_deps" "class_deps" "thm_deps" "print_term_bindings"
    85     "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
    86     "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
    87   and "print_state" :: diag
    88   and "welcome" :: diag
    89   and "end" :: thy_end
    90   and "realizers" :: thy_decl
    91   and "realizability" :: thy_decl
    92   and "extract_type" "extract" :: thy_decl
    93   and "find_theorems" "find_consts" :: diag
    94   and "named_theorems" :: thy_decl
    95 abbrevs "===>" = "===>"  (*prevent replacement of very long arrows*)
    96   and "--->" = "\<midarrow>\<rightarrow>"
    97   and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = ""
    98   and "hence" = "then have"
    99   and "thus" = "then show"
   100 begin
   101 
   102 section \<open>Isar commands\<close>
   103 
   104 subsection \<open>Other files\<close>
   105 
   106 ML \<open>
   107 local
   108   val _ =
   109     Outer_Syntax.command \<^command_keyword>\<open>external_file\<close> "formal dependency on external file"
   110       (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files)));
   111 
   112   val _ =
   113     Outer_Syntax.command \<^command_keyword>\<open>bibtex_file\<close> "check bibtex database file in Prover IDE"
   114       (Resources.provide_parse_files "bibtex_file" >> (fn files =>
   115         Toplevel.theory (fn thy =>
   116           let
   117             val ([{lines, pos, ...}], thy') = files thy;
   118             val _ = Bibtex.check_database_output pos (cat_lines lines);
   119           in thy' end)));
   120 in end\<close>
   121 
   122 
   123 subsection \<open>Embedded ML text\<close>
   124 
   125 ML \<open>
   126 local
   127 
   128 val semi = Scan.option \<^keyword>\<open>;\<close>;
   129 
   130 val _ =
   131   Outer_Syntax.command \<^command_keyword>\<open>ML_file\<close> "read and evaluate Isabelle/ML file"
   132     (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE);
   133 
   134 val _ =
   135   Outer_Syntax.command \<^command_keyword>\<open>ML_file_debug\<close>
   136     "read and evaluate Isabelle/ML file (with debugger information)"
   137     (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true));
   138 
   139 val _ =
   140   Outer_Syntax.command \<^command_keyword>\<open>ML_file_no_debug\<close>
   141     "read and evaluate Isabelle/ML file (no debugger information)"
   142     (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false));
   143 
   144 val _ =
   145   Outer_Syntax.command \<^command_keyword>\<open>SML_file\<close> "read and evaluate Standard ML file"
   146     (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE);
   147 
   148 val _ =
   149   Outer_Syntax.command \<^command_keyword>\<open>SML_file_debug\<close>
   150     "read and evaluate Standard ML file (with debugger information)"
   151     (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true));
   152 
   153 val _ =
   154   Outer_Syntax.command \<^command_keyword>\<open>SML_file_no_debug\<close>
   155     "read and evaluate Standard ML file (no debugger information)"
   156     (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false));
   157 
   158 val _ =
   159   Outer_Syntax.command \<^command_keyword>\<open>SML_export\<close> "evaluate SML within Isabelle/ML environment"
   160     (Parse.ML_source >> (fn source =>
   161       let
   162         val flags: ML_Compiler.flags =
   163           {environment = ML_Env.SML_export, redirect = false, verbose = true,
   164             debug = NONE, writeln = writeln, warning = warning};
   165       in
   166         Toplevel.theory
   167           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
   168       end));
   169 
   170 val _ =
   171   Outer_Syntax.command \<^command_keyword>\<open>SML_import\<close> "evaluate Isabelle/ML within SML environment"
   172     (Parse.ML_source >> (fn source =>
   173       let
   174         val flags: ML_Compiler.flags =
   175           {environment = ML_Env.SML_import, redirect = false, verbose = true,
   176             debug = NONE, writeln = writeln, warning = warning};
   177       in
   178         Toplevel.generic_theory
   179           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
   180             Local_Theory.propagate_ml_env)
   181       end));
   182 
   183 val _ =
   184   Outer_Syntax.command ("ML_export", \<^here>)
   185     "ML text within theory or local theory, and export to bootstrap environment"
   186     (Parse.ML_source >> (fn source =>
   187       Toplevel.generic_theory (fn context =>
   188         context
   189         |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle
   190         |> Config.put_generic ML_Env.ML_write_global true
   191         |> ML_Context.exec (fn () =>
   192             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
   193         |> Config.restore_generic ML_Env.ML_write_global context
   194         |> Config.restore_generic ML_Env.ML_environment context
   195         |> Local_Theory.propagate_ml_env)));
   196 
   197 val _ =
   198   Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
   199     (Parse.ML_source >> (fn source =>
   200       Toplevel.proof (Proof.map_context (Context.proof_map
   201         (ML_Context.exec (fn () =>
   202             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #>
   203           Proof.propagate_ml_env)));
   204 
   205 val _ =
   206   Outer_Syntax.command \<^command_keyword>\<open>ML_val\<close> "diagnostic ML text"
   207     (Parse.ML_source >> Isar_Cmd.ml_diag true);
   208 
   209 val _ =
   210   Outer_Syntax.command \<^command_keyword>\<open>ML_command\<close> "diagnostic ML text (silent)"
   211     (Parse.ML_source >> Isar_Cmd.ml_diag false);
   212 
   213 val _ =
   214   Outer_Syntax.command \<^command_keyword>\<open>setup\<close> "ML setup for global theory"
   215     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup));
   216 
   217 val _ =
   218   Outer_Syntax.local_theory \<^command_keyword>\<open>local_setup\<close> "ML setup for local theory"
   219     (Parse.ML_source >> Isar_Cmd.local_setup);
   220 
   221 val _ =
   222   Outer_Syntax.command \<^command_keyword>\<open>oracle\<close> "declare oracle"
   223     (Parse.range Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.ML_source) >>
   224       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
   225 
   226 val _ =
   227   Outer_Syntax.local_theory \<^command_keyword>\<open>attribute_setup\<close> "define attribute in ML"
   228     (Parse.position Parse.name --
   229         Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
   230       >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
   231 
   232 val _ =
   233   Outer_Syntax.local_theory \<^command_keyword>\<open>method_setup\<close> "define proof method in ML"
   234     (Parse.position Parse.name --
   235         Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
   236       >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
   237 
   238 val _ =
   239   Outer_Syntax.local_theory \<^command_keyword>\<open>declaration\<close> "generic ML declaration"
   240     (Parse.opt_keyword "pervasive" -- Parse.ML_source
   241       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
   242 
   243 val _ =
   244   Outer_Syntax.local_theory \<^command_keyword>\<open>syntax_declaration\<close> "generic ML syntax declaration"
   245     (Parse.opt_keyword "pervasive" -- Parse.ML_source
   246       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
   247 
   248 val _ =
   249   Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
   250     (Parse.position Parse.name --
   251       (\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close> --| \<^keyword>\<open>=\<close>) --
   252       Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
   253 
   254 in end\<close>
   255 
   256 
   257 subsection \<open>Theory commands\<close>
   258 
   259 subsubsection \<open>Sorts and types\<close>
   260 
   261 ML \<open>
   262 local
   263 
   264 val _ =
   265   Outer_Syntax.local_theory \<^command_keyword>\<open>default_sort\<close>
   266     "declare default sort for explicit type variables"
   267     (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   268 
   269 val _ =
   270   Outer_Syntax.local_theory \<^command_keyword>\<open>typedecl\<close> "type declaration"
   271     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
   272       >> (fn ((args, a), mx) =>
   273           Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
   274 
   275 val _ =
   276   Outer_Syntax.local_theory \<^command_keyword>\<open>type_synonym\<close> "declare type abbreviation"
   277     (Parse.type_args -- Parse.binding --
   278       (\<^keyword>\<open>=\<close> |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
   279       >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
   280 
   281 in end\<close>
   282 
   283 
   284 subsubsection \<open>Consts\<close>
   285 
   286 ML \<open>
   287 local
   288 
   289 val _ =
   290   Outer_Syntax.command \<^command_keyword>\<open>judgment\<close> "declare object-logic judgment"
   291     (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   292 
   293 val _ =
   294   Outer_Syntax.command \<^command_keyword>\<open>consts\<close> "declare constants"
   295     (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
   296 
   297 in end\<close>
   298 
   299 
   300 subsubsection \<open>Syntax and translations\<close>
   301 
   302 ML \<open>
   303 local
   304 
   305 val _ =
   306   Outer_Syntax.command \<^command_keyword>\<open>nonterminal\<close>
   307     "declare syntactic type constructors (grammar nonterminal symbols)"
   308     (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
   309 
   310 val _ =
   311   Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
   312     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
   313       >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
   314 
   315 val _ =
   316   Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
   317     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
   318       >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
   319 
   320 val trans_pat =
   321   Scan.optional
   322     (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\<open>)\<close>)) "logic"
   323     -- Parse.inner_syntax Parse.string;
   324 
   325 fun trans_arrow toks =
   326   ((\<^keyword>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>) >> K Syntax.Parse_Rule ||
   327     (\<^keyword>\<open>\<leftharpoondown>\<close> || \<^keyword>\<open><=\<close>) >> K Syntax.Print_Rule ||
   328     (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) >> K Syntax.Parse_Print_Rule) toks;
   329 
   330 val trans_line =
   331   trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
   332     >> (fn (left, (arr, right)) => arr (left, right));
   333 
   334 val _ =
   335   Outer_Syntax.command \<^command_keyword>\<open>translations\<close> "add syntax translation rules"
   336     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
   337 
   338 val _ =
   339   Outer_Syntax.command \<^command_keyword>\<open>no_translations\<close> "delete syntax translation rules"
   340     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
   341 
   342 in end\<close>
   343 
   344 
   345 subsubsection \<open>Translation functions\<close>
   346 
   347 ML \<open>
   348 local
   349 
   350 val _ =
   351   Outer_Syntax.command \<^command_keyword>\<open>parse_ast_translation\<close>
   352     "install parse ast translation functions"
   353     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
   354 
   355 val _ =
   356   Outer_Syntax.command \<^command_keyword>\<open>parse_translation\<close>
   357     "install parse translation functions"
   358     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
   359 
   360 val _ =
   361   Outer_Syntax.command \<^command_keyword>\<open>print_translation\<close>
   362     "install print translation functions"
   363     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
   364 
   365 val _ =
   366   Outer_Syntax.command \<^command_keyword>\<open>typed_print_translation\<close>
   367     "install typed print translation functions"
   368     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
   369 
   370 val _ =
   371   Outer_Syntax.command \<^command_keyword>\<open>print_ast_translation\<close>
   372     "install print ast translation functions"
   373     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
   374 
   375 in end\<close>
   376 
   377 
   378 subsubsection \<open>Specifications\<close>
   379 
   380 ML \<open>
   381 local
   382 
   383 val _ =
   384   Outer_Syntax.local_theory' \<^command_keyword>\<open>definition\<close> "constant definition"
   385     (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
   386       Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
   387         #2 oo Specification.definition_cmd decl params prems spec));
   388 
   389 val _ =
   390   Outer_Syntax.local_theory' \<^command_keyword>\<open>abbreviation\<close> "constant abbreviation"
   391     (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
   392       >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
   393 
   394 val axiomatization =
   395   Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --
   396   Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
   397 
   398 val _ =
   399   Outer_Syntax.command \<^command_keyword>\<open>axiomatization\<close> "axiomatic constant specification"
   400     (Scan.optional Parse.vars [] --
   401       Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
   402       >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
   403 
   404 val _ =
   405   Outer_Syntax.local_theory \<^command_keyword>\<open>alias\<close> "name-space alias for constant"
   406     (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.position Parse.name)
   407       >> Specification.alias_cmd);
   408 
   409 val _ =
   410   Outer_Syntax.local_theory \<^command_keyword>\<open>type_alias\<close> "name-space alias for type constructor"
   411     (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.position Parse.name)
   412       >> Specification.type_alias_cmd);
   413 
   414 in end\<close>
   415 
   416 
   417 subsubsection \<open>Notation\<close>
   418 
   419 ML \<open>
   420 local
   421 
   422 val _ =
   423   Outer_Syntax.local_theory \<^command_keyword>\<open>type_notation\<close>
   424     "add concrete syntax for type constructors"
   425     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   426       >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   427 
   428 val _ =
   429   Outer_Syntax.local_theory \<^command_keyword>\<open>no_type_notation\<close>
   430     "delete concrete syntax for type constructors"
   431     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   432       >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   433 
   434 val _ =
   435   Outer_Syntax.local_theory \<^command_keyword>\<open>notation\<close>
   436     "add concrete syntax for constants / fixed variables"
   437     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   438       >> (fn (mode, args) => Specification.notation_cmd true mode args));
   439 
   440 val _ =
   441   Outer_Syntax.local_theory \<^command_keyword>\<open>no_notation\<close>
   442     "delete concrete syntax for constants / fixed variables"
   443     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   444       >> (fn (mode, args) => Specification.notation_cmd false mode args));
   445 
   446 in end\<close>
   447 
   448 
   449 subsubsection \<open>Theorems\<close>
   450 
   451 ML \<open>
   452 local
   453 
   454 val long_keyword =
   455   Parse_Spec.includes >> K "" ||
   456   Parse_Spec.long_statement_keyword;
   457 
   458 val long_statement =
   459   Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
   460   Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
   461     >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
   462 
   463 val short_statement =
   464   Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
   465     >> (fn ((shows, assumes), fixes) =>
   466       (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes],
   467         Element.Shows shows));
   468 
   469 fun theorem spec schematic descr =
   470   Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr)
   471     ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) =>
   472       ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
   473         long Thm.theoremK NONE (K I) binding includes elems concl)));
   474 
   475 val _ = theorem \<^command_keyword>\<open>theorem\<close> false "theorem";
   476 val _ = theorem \<^command_keyword>\<open>lemma\<close> false "lemma";
   477 val _ = theorem \<^command_keyword>\<open>corollary\<close> false "corollary";
   478 val _ = theorem \<^command_keyword>\<open>proposition\<close> false "proposition";
   479 val _ = theorem \<^command_keyword>\<open>schematic_goal\<close> true "schematic goal";
   480 
   481 in end\<close>
   482 
   483 ML \<open>
   484 local
   485 
   486 val _ =
   487   Outer_Syntax.local_theory' \<^command_keyword>\<open>lemmas\<close> "define theorems"
   488     (Parse_Spec.name_facts -- Parse.for_fixes >>
   489       (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
   490 
   491 val _ =
   492   Outer_Syntax.local_theory' \<^command_keyword>\<open>declare\<close> "declare theorems"
   493     (Parse.and_list1 Parse.thms1 -- Parse.for_fixes
   494       >> (fn (facts, fixes) =>
   495           #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes));
   496 
   497 val _ =
   498   Outer_Syntax.local_theory \<^command_keyword>\<open>named_theorems\<close>
   499     "declare named collection of theorems"
   500     (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   501       fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
   502 
   503 in end\<close>
   504 
   505 
   506 subsubsection \<open>Hide names\<close>
   507 
   508 ML \<open>
   509 local
   510 
   511 fun hide_names command_keyword what hide parse prep =
   512   Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
   513     ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
   514       (Toplevel.theory (fn thy =>
   515         let val ctxt = Proof_Context.init_global thy
   516         in fold (hide fully o prep ctxt) args thy end))));
   517 
   518 val _ =
   519   hide_names \<^command_keyword>\<open>hide_class\<close> "classes" Sign.hide_class Parse.class
   520     Proof_Context.read_class;
   521 
   522 val _ =
   523   hide_names \<^command_keyword>\<open>hide_type\<close> "types" Sign.hide_type Parse.type_const
   524     ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
   525 
   526 val _ =
   527   hide_names \<^command_keyword>\<open>hide_const\<close> "consts" Sign.hide_const Parse.const
   528     ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
   529 
   530 val _ =
   531   hide_names \<^command_keyword>\<open>hide_fact\<close> "facts" Global_Theory.hide_fact
   532     (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
   533 
   534 in end\<close>
   535 
   536 
   537 subsection \<open>Bundled declarations\<close>
   538 
   539 ML \<open>
   540 local
   541 
   542 val _ =
   543   Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>bundle\<close>
   544     "define bundle of declarations"
   545     ((Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
   546       >> (uncurry Bundle.bundle_cmd))
   547     (Parse.binding --| Parse.begin >> Bundle.init);
   548 
   549 val _ =
   550   Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
   551     "activate declarations from bundle in local theory"
   552     (Scan.repeat1 (Parse.position Parse.name) >> Bundle.unbundle_cmd);
   553 
   554 val _ =
   555   Outer_Syntax.command \<^command_keyword>\<open>include\<close>
   556     "activate declarations from bundle in proof body"
   557     (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
   558 
   559 val _ =
   560   Outer_Syntax.command \<^command_keyword>\<open>including\<close>
   561     "activate declarations from bundle in goal refinement"
   562     (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
   563 
   564 val _ =
   565   Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>
   566     "print bundles of declarations"
   567     (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
   568 
   569 in end\<close>
   570 
   571 
   572 subsection \<open>Local theory specifications\<close>
   573 
   574 subsubsection \<open>Specification context\<close>
   575 
   576 ML \<open>
   577 local
   578 
   579 val _ =
   580   Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
   581     ((Parse.position Parse.name >> (fn name =>
   582         Toplevel.begin_local_theory true (Named_Target.begin name)) ||
   583       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
   584         >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
   585       --| Parse.begin);
   586 
   587 val _ =
   588   Outer_Syntax.command \<^command_keyword>\<open>end\<close> "end context"
   589     (Scan.succeed
   590       (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
   591         Toplevel.end_proof (K Proof.end_notepad)));
   592 
   593 in end\<close>
   594 
   595 
   596 subsubsection \<open>Locales and interpretation\<close>
   597 
   598 ML \<open>
   599 local
   600 
   601 val locale_val =
   602   Parse_Spec.locale_expression --
   603     Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   604   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
   605 
   606 val _ =
   607   Outer_Syntax.command \<^command_keyword>\<open>locale\<close> "define named specification context"
   608     (Parse.binding --
   609       Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
   610       >> (fn ((name, (expr, elems)), begin) =>
   611           Toplevel.begin_local_theory begin
   612             (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
   613 
   614 val _ =
   615   Outer_Syntax.command \<^command_keyword>\<open>experiment\<close> "open private specification context"
   616     (Scan.repeat Parse_Spec.context_element --| Parse.begin
   617       >> (fn elems =>
   618           Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
   619 
   620 val _ =
   621   Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
   622     "prove interpretation of locale expression in proof context"
   623     (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
   624       Toplevel.proof (Interpretation.interpret_cmd expr)));
   625 
   626 val interpretation_args_with_defs =
   627   Parse.!!! Parse_Spec.locale_expression --
   628     (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   629       -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) ([]));
   630 
   631 val _ =
   632   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
   633     "prove interpretation of locale expression into global theory"
   634     (interpretation_args_with_defs >> (fn (expr, defs) =>
   635       Interpretation.global_interpretation_cmd expr defs));
   636 
   637 val _ =
   638   Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
   639     "prove sublocale relation between a locale and a locale expression"
   640     ((Parse.position Parse.name --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
   641       interpretation_args_with_defs >> (fn (loc, (expr, defs)) =>
   642         Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs)))
   643     || interpretation_args_with_defs >> (fn (expr, defs) =>
   644         Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs)));
   645 
   646 val _ =
   647   Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
   648     "prove interpretation of locale expression in local theory or into global theory"
   649     (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
   650       Toplevel.local_theory_to_proof NONE NONE
   651         (Interpretation.isar_interpretation_cmd expr)));
   652 
   653 in end\<close>
   654 
   655 
   656 subsubsection \<open>Type classes\<close>
   657 
   658 ML \<open>
   659 local
   660 
   661 val class_val =
   662   Parse_Spec.class_expression --
   663     Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   664   Scan.repeat1 Parse_Spec.context_element >> pair [];
   665 
   666 val _ =
   667   Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
   668    (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], []) -- Parse.opt_begin
   669     >> (fn ((name, (supclasses, elems)), begin) =>
   670         Toplevel.begin_local_theory begin
   671           (Class_Declaration.class_cmd name supclasses elems #> snd)));
   672 
   673 val _ =
   674   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>subclass\<close> "prove a subclass relation"
   675     (Parse.class >> Class_Declaration.subclass_cmd);
   676 
   677 val _ =
   678   Outer_Syntax.command \<^command_keyword>\<open>instantiation\<close> "instantiate and prove type arity"
   679    (Parse.multi_arity --| Parse.begin
   680      >> (fn arities => Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
   681 
   682 val _ =
   683   Outer_Syntax.command \<^command_keyword>\<open>instance\<close> "prove type arity or subclass relation"
   684   ((Parse.class --
   685     ((\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
   686     Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
   687     Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
   688 
   689 in end\<close>
   690 
   691 
   692 subsubsection \<open>Arbitrary overloading\<close>
   693 
   694 ML \<open>
   695 local
   696 
   697 val _ =
   698   Outer_Syntax.command \<^command_keyword>\<open>overloading\<close> "overloaded definitions"
   699    (Scan.repeat1 (Parse.name --| (\<^keyword>\<open>==\<close> || \<^keyword>\<open>\<equiv>\<close>) -- Parse.term --
   700       Scan.optional (\<^keyword>\<open>(\<close> |-- (\<^keyword>\<open>unchecked\<close> >> K false) --| \<^keyword>\<open>)\<close>) true
   701       >> Scan.triple1) --| Parse.begin
   702    >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
   703 
   704 in end\<close>
   705 
   706 
   707 subsection \<open>Proof commands\<close>
   708 
   709 ML \<open>
   710 local
   711 
   712 val _ =
   713   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>notepad\<close> "begin proof context"
   714     (Parse.begin >> K Proof.begin_notepad);
   715 
   716 in end\<close>
   717 
   718 
   719 subsubsection \<open>Statements\<close>
   720 
   721 ML \<open>
   722 local
   723 
   724 val structured_statement =
   725   Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
   726     >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
   727 
   728 val _ =
   729   Outer_Syntax.command \<^command_keyword>\<open>have\<close> "state local goal"
   730     (structured_statement >> (fn (a, b, c, d) =>
   731       Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2)));
   732 
   733 val _ =
   734   Outer_Syntax.command \<^command_keyword>\<open>show\<close> "state local goal, to refine pending subgoals"
   735     (structured_statement >> (fn (a, b, c, d) =>
   736       Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2)));
   737 
   738 val _ =
   739   Outer_Syntax.command \<^command_keyword>\<open>hence\<close> "old-style alias of \"then have\""
   740     (structured_statement >> (fn (a, b, c, d) =>
   741       Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2)));
   742 
   743 val _ =
   744   Outer_Syntax.command \<^command_keyword>\<open>thus\<close> "old-style alias of  \"then show\""
   745     (structured_statement >> (fn (a, b, c, d) =>
   746       Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
   747 
   748 in end\<close>
   749 
   750 
   751 subsubsection \<open>Local facts\<close>
   752 
   753 ML \<open>
   754 local
   755 
   756 val facts = Parse.and_list1 Parse.thms1;
   757 
   758 val _ =
   759   Outer_Syntax.command \<^command_keyword>\<open>then\<close> "forward chaining"
   760     (Scan.succeed (Toplevel.proof Proof.chain));
   761 
   762 val _ =
   763   Outer_Syntax.command \<^command_keyword>\<open>from\<close> "forward chaining from given facts"
   764     (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
   765 
   766 val _ =
   767   Outer_Syntax.command \<^command_keyword>\<open>with\<close> "forward chaining from given and current facts"
   768     (facts >> (Toplevel.proof o Proof.with_thmss_cmd));
   769 
   770 val _ =
   771   Outer_Syntax.command \<^command_keyword>\<open>note\<close> "define facts"
   772     (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd));
   773 
   774 val _ =
   775   Outer_Syntax.command \<^command_keyword>\<open>supply\<close> "define facts during goal refinement (unstructured)"
   776     (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd));
   777 
   778 val _ =
   779   Outer_Syntax.command \<^command_keyword>\<open>using\<close> "augment goal facts"
   780     (facts >> (Toplevel.proof o Proof.using_cmd));
   781 
   782 val _ =
   783   Outer_Syntax.command \<^command_keyword>\<open>unfolding\<close> "unfold definitions in goal and facts"
   784     (facts >> (Toplevel.proof o Proof.unfolding_cmd));
   785 
   786 in end\<close>
   787 
   788 
   789 subsubsection \<open>Proof context\<close>
   790 
   791 ML \<open>
   792 local
   793 
   794 val structured_statement =
   795   Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
   796     >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   797 
   798 val _ =
   799   Outer_Syntax.command \<^command_keyword>\<open>fix\<close> "fix local variables (Skolem constants)"
   800     (Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
   801 
   802 val _ =
   803   Outer_Syntax.command \<^command_keyword>\<open>assume\<close> "assume propositions"
   804     (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
   805 
   806 val _ =
   807   Outer_Syntax.command \<^command_keyword>\<open>presume\<close> "assume propositions, to be established later"
   808     (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
   809 
   810 val _ =
   811   Outer_Syntax.command \<^command_keyword>\<open>define\<close> "local definition (non-polymorphic)"
   812     ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
   813       >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
   814 
   815 val _ =
   816   Outer_Syntax.command \<^command_keyword>\<open>consider\<close> "state cases rule"
   817     (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
   818 
   819 val _ =
   820   Outer_Syntax.command \<^command_keyword>\<open>obtain\<close> "generalized elimination"
   821     (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
   822       >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
   823 
   824 val _ =
   825   Outer_Syntax.command \<^command_keyword>\<open>guess\<close> "wild guessing (unstructured)"
   826     (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
   827 
   828 val _ =
   829   Outer_Syntax.command \<^command_keyword>\<open>let\<close> "bind text variables"
   830     (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\<open>=\<close> |-- Parse.term))
   831       >> (Toplevel.proof o Proof.let_bind_cmd));
   832 
   833 val _ =
   834   Outer_Syntax.command \<^command_keyword>\<open>write\<close> "add concrete syntax for constants / fixed variables"
   835     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   836     >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
   837 
   838 val _ =
   839   Outer_Syntax.command \<^command_keyword>\<open>case\<close> "invoke local context"
   840     (Parse_Spec.opt_thm_name ":" --
   841       (\<^keyword>\<open>(\<close> |--
   842         Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
   843           --| \<^keyword>\<open>)\<close>) ||
   844         Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   845 
   846 in end\<close>
   847 
   848 
   849 subsubsection \<open>Proof structure\<close>
   850 
   851 ML \<open>
   852 local
   853 
   854 val _ =
   855   Outer_Syntax.command \<^command_keyword>\<open>{\<close> "begin explicit proof block"
   856     (Scan.succeed (Toplevel.proof Proof.begin_block));
   857 
   858 val _ =
   859   Outer_Syntax.command \<^command_keyword>\<open>}\<close> "end explicit proof block"
   860     (Scan.succeed (Toplevel.proof Proof.end_block));
   861 
   862 val _ =
   863   Outer_Syntax.command \<^command_keyword>\<open>next\<close> "enter next proof block"
   864     (Scan.succeed (Toplevel.proof Proof.next_block));
   865 
   866 in end\<close>
   867 
   868 
   869 subsubsection \<open>End proof\<close>
   870 
   871 ML \<open>
   872 local
   873 
   874 val _ =
   875   Outer_Syntax.command \<^command_keyword>\<open>qed\<close> "conclude proof"
   876     (Scan.option Method.parse >> (fn m =>
   877      (Option.map Method.report m;
   878       Isar_Cmd.qed m)));
   879 
   880 val _ =
   881   Outer_Syntax.command \<^command_keyword>\<open>by\<close> "terminal backward proof"
   882     (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
   883      (Method.report m1;
   884       Option.map Method.report m2;
   885       Isar_Cmd.terminal_proof (m1, m2))));
   886 
   887 val _ =
   888   Outer_Syntax.command \<^command_keyword>\<open>..\<close> "default proof"
   889     (Scan.succeed Isar_Cmd.default_proof);
   890 
   891 val _ =
   892   Outer_Syntax.command \<^command_keyword>\<open>.\<close> "immediate proof"
   893     (Scan.succeed Isar_Cmd.immediate_proof);
   894 
   895 val _ =
   896   Outer_Syntax.command \<^command_keyword>\<open>done\<close> "done proof"
   897     (Scan.succeed Isar_Cmd.done_proof);
   898 
   899 val _ =
   900   Outer_Syntax.command \<^command_keyword>\<open>sorry\<close> "skip proof (quick-and-dirty mode only!)"
   901     (Scan.succeed Isar_Cmd.skip_proof);
   902 
   903 val _ =
   904   Outer_Syntax.command \<^command_keyword>\<open>\<proof>\<close> "dummy proof (quick-and-dirty mode only!)"
   905     (Scan.succeed Isar_Cmd.skip_proof);
   906 
   907 val _ =
   908   Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
   909     (Scan.succeed Toplevel.forget_proof);
   910 
   911 in end\<close>
   912 
   913 
   914 subsubsection \<open>Proof steps\<close>
   915 
   916 ML \<open>
   917 local
   918 
   919 val _ =
   920   Outer_Syntax.command \<^command_keyword>\<open>defer\<close> "shuffle internal proof state"
   921     (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer));
   922 
   923 val _ =
   924   Outer_Syntax.command \<^command_keyword>\<open>prefer\<close> "shuffle internal proof state"
   925     (Parse.nat >> (Toplevel.proof o Proof.prefer));
   926 
   927 val _ =
   928   Outer_Syntax.command \<^command_keyword>\<open>apply\<close> "initial goal refinement step (unstructured)"
   929     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
   930 
   931 val _ =
   932   Outer_Syntax.command \<^command_keyword>\<open>apply_end\<close> "terminal goal refinement step (unstructured)"
   933     (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
   934 
   935 val _ =
   936   Outer_Syntax.command \<^command_keyword>\<open>proof\<close> "backward proof step"
   937     (Scan.option Method.parse >> (fn m =>
   938       (Option.map Method.report m;
   939        Toplevel.proof (fn state =>
   940          let
   941           val state' = state |> Proof.proof m |> Seq.the_result "";
   942           val _ =
   943             Output.information
   944               (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state'));
   945         in state' end))))
   946 
   947 in end\<close>
   948 
   949 
   950 subsubsection \<open>Subgoal focus\<close>
   951 
   952 ML \<open>
   953 local
   954 
   955 val opt_fact_binding =
   956   Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
   957     Binding.empty_atts;
   958 
   959 val for_params =
   960   Scan.optional
   961     (\<^keyword>\<open>for\<close> |--
   962       Parse.!!! ((Scan.option Parse.dots >> is_some) --
   963         (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
   964     (false, []);
   965 
   966 val _ =
   967   Outer_Syntax.command \<^command_keyword>\<open>subgoal\<close>
   968     "focus on first subgoal within backward refinement"
   969     (opt_fact_binding -- (Scan.option (\<^keyword>\<open>premises\<close> |-- Parse.!!! opt_fact_binding)) --
   970       for_params >> (fn ((a, b), c) =>
   971         Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
   972 
   973 in end\<close>
   974 
   975 
   976 subsubsection \<open>Calculation\<close>
   977 
   978 ML \<open>
   979 local
   980 
   981 val calculation_args =
   982   Scan.option (\<^keyword>\<open>(\<close> |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\<open>)\<close>)));
   983 
   984 val _ =
   985   Outer_Syntax.command \<^command_keyword>\<open>also\<close> "combine calculation and current facts"
   986     (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
   987 
   988 val _ =
   989   Outer_Syntax.command \<^command_keyword>\<open>finally\<close>
   990     "combine calculation and current facts, exhibit result"
   991     (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
   992 
   993 val _ =
   994   Outer_Syntax.command \<^command_keyword>\<open>moreover\<close> "augment calculation by current facts"
   995     (Scan.succeed (Toplevel.proof' Calculation.moreover));
   996 
   997 val _ =
   998   Outer_Syntax.command \<^command_keyword>\<open>ultimately\<close>
   999     "augment calculation by current facts, exhibit result"
  1000     (Scan.succeed (Toplevel.proof' Calculation.ultimately));
  1001 
  1002 val _ =
  1003   Outer_Syntax.command \<^command_keyword>\<open>print_trans_rules\<close> "print transitivity rules"
  1004     (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
  1005 
  1006 in end\<close>
  1007 
  1008 
  1009 subsubsection \<open>Proof navigation\<close>
  1010 
  1011 ML \<open>
  1012 local
  1013 
  1014 fun report_back () =
  1015   Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
  1016 
  1017 val _ =
  1018   Outer_Syntax.command \<^command_keyword>\<open>back\<close> "explicit backtracking of proof command"
  1019     (Scan.succeed
  1020      (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
  1021       Toplevel.skip_proof report_back));
  1022 
  1023 in end\<close>
  1024 
  1025 
  1026 subsection \<open>Diagnostic commands (for interactive mode only)\<close>
  1027 
  1028 ML \<open>
  1029 local
  1030 
  1031 val opt_modes =
  1032   Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
  1033 
  1034 val _ =
  1035   Outer_Syntax.command \<^command_keyword>\<open>help\<close>
  1036     "retrieve outer syntax commands according to name patterns"
  1037     (Scan.repeat Parse.name >>
  1038       (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats)));
  1039 
  1040 val _ =
  1041   Outer_Syntax.command \<^command_keyword>\<open>print_commands\<close> "print outer syntax commands"
  1042     (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of)));
  1043 
  1044 val _ =
  1045   Outer_Syntax.command \<^command_keyword>\<open>print_options\<close> "print configuration options"
  1046     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
  1047 
  1048 val _ =
  1049   Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
  1050     "print context of local theory target"
  1051     (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
  1052 
  1053 val _ =
  1054   Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
  1055     "print logical theory contents"
  1056     (Parse.opt_bang >> (fn b =>
  1057       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of)));
  1058 
  1059 val _ =
  1060   Outer_Syntax.command \<^command_keyword>\<open>print_definitions\<close>
  1061     "print dependencies of definitional theory content"
  1062     (Parse.opt_bang >> (fn b =>
  1063       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of)));
  1064 
  1065 val _ =
  1066   Outer_Syntax.command \<^command_keyword>\<open>print_syntax\<close>
  1067     "print inner syntax of context"
  1068     (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
  1069 
  1070 val _ =
  1071   Outer_Syntax.command \<^command_keyword>\<open>print_defn_rules\<close>
  1072     "print definitional rewrite rules of context"
  1073     (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
  1074 
  1075 val _ =
  1076   Outer_Syntax.command \<^command_keyword>\<open>print_abbrevs\<close>
  1077     "print constant abbreviations of context"
  1078     (Parse.opt_bang >> (fn b =>
  1079       Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
  1080 
  1081 val _ =
  1082   Outer_Syntax.command \<^command_keyword>\<open>print_theorems\<close>
  1083     "print theorems of local theory or proof context"
  1084     (Parse.opt_bang >> (fn b =>
  1085       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
  1086 
  1087 val _ =
  1088   Outer_Syntax.command \<^command_keyword>\<open>print_locales\<close>
  1089     "print locales of this theory"
  1090     (Parse.opt_bang >> (fn verbose =>
  1091       Toplevel.keep (fn state =>
  1092         let val thy = Toplevel.theory_of state
  1093         in Pretty.writeln (Locale.pretty_locales thy verbose) end)));
  1094 
  1095 val _ =
  1096   Outer_Syntax.command \<^command_keyword>\<open>print_classes\<close>
  1097     "print classes of this theory"
  1098     (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
  1099 
  1100 val _ =
  1101   Outer_Syntax.command \<^command_keyword>\<open>print_locale\<close>
  1102     "print locale of this theory"
  1103     (Parse.opt_bang -- Parse.position Parse.name >> (fn (show_facts, raw_name) =>
  1104       Toplevel.keep (fn state =>
  1105         let
  1106           val thy = Toplevel.theory_of state;
  1107           val name = Locale.check thy raw_name;
  1108         in Pretty.writeln (Locale.pretty_locale thy show_facts name) end)));
  1109 
  1110 val _ =
  1111   Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
  1112     "print interpretations of locale for this theory or proof context"
  1113     (Parse.position Parse.name >> (fn raw_name =>
  1114       Toplevel.keep (fn state =>
  1115         let
  1116           val ctxt = Toplevel.context_of state;
  1117           val thy = Toplevel.theory_of state;
  1118           val name = Locale.check thy raw_name;
  1119         in Pretty.writeln (Locale.pretty_registrations ctxt name) end)));
  1120 
  1121 val _ =
  1122   Outer_Syntax.command \<^command_keyword>\<open>print_dependencies\<close>
  1123     "print dependencies of locale expression"
  1124     (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (clean, expr) =>
  1125       Toplevel.keep (fn state =>
  1126         Pretty.writeln (Expression.pretty_dependencies (Toplevel.context_of state) clean expr))));
  1127 
  1128 val _ =
  1129   Outer_Syntax.command \<^command_keyword>\<open>print_attributes\<close>
  1130     "print attributes of this theory"
  1131     (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
  1132 
  1133 val _ =
  1134   Outer_Syntax.command \<^command_keyword>\<open>print_simpset\<close>
  1135     "print context of Simplifier"
  1136     (Parse.opt_bang >> (fn b =>
  1137       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
  1138 
  1139 val _ =
  1140   Outer_Syntax.command \<^command_keyword>\<open>print_rules\<close> "print intro/elim rules"
  1141     (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
  1142 
  1143 val _ =
  1144   Outer_Syntax.command \<^command_keyword>\<open>print_methods\<close> "print methods of this theory"
  1145     (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
  1146 
  1147 val _ =
  1148   Outer_Syntax.command \<^command_keyword>\<open>print_antiquotations\<close>
  1149     "print document antiquotations"
  1150     (Parse.opt_bang >> (fn b =>
  1151       Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of)));
  1152 
  1153 val _ =
  1154   Outer_Syntax.command \<^command_keyword>\<open>print_ML_antiquotations\<close>
  1155     "print ML antiquotations"
  1156     (Parse.opt_bang >> (fn b =>
  1157       Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
  1158 
  1159 val _ =
  1160   Outer_Syntax.command \<^command_keyword>\<open>locale_deps\<close> "visualize locale dependencies"
  1161     (Scan.succeed
  1162       (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
  1163         Locale.pretty_locale_deps thy
  1164         |> map (fn {name, parents, body} =>
  1165           ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
  1166         |> Graph_Display.display_graph_old))));
  1167 
  1168 val _ =
  1169   Outer_Syntax.command \<^command_keyword>\<open>print_term_bindings\<close>
  1170     "print term bindings of proof context"
  1171     (Scan.succeed
  1172       (Toplevel.keep
  1173         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
  1174 
  1175 val _ =
  1176   Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
  1177     (Parse.opt_bang >> (fn b =>
  1178       Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
  1179 
  1180 val _ =
  1181   Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
  1182     (Scan.succeed
  1183       (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
  1184 
  1185 val _ =
  1186   Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
  1187     "print theorems as long statements"
  1188     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts);
  1189 
  1190 val _ =
  1191   Outer_Syntax.command \<^command_keyword>\<open>thm\<close> "print theorems"
  1192     (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms);
  1193 
  1194 val _ =
  1195   Outer_Syntax.command \<^command_keyword>\<open>prf\<close> "print proof terms of theorems"
  1196     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false);
  1197 
  1198 val _ =
  1199   Outer_Syntax.command \<^command_keyword>\<open>full_prf\<close> "print full proof terms of theorems"
  1200     (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true);
  1201 
  1202 val _ =
  1203   Outer_Syntax.command \<^command_keyword>\<open>prop\<close> "read and print proposition"
  1204     (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
  1205 
  1206 val _ =
  1207   Outer_Syntax.command \<^command_keyword>\<open>term\<close> "read and print term"
  1208     (opt_modes -- Parse.term >> Isar_Cmd.print_term);
  1209 
  1210 val _ =
  1211   Outer_Syntax.command \<^command_keyword>\<open>typ\<close> "read and print type"
  1212     (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\<open>::\<close> |-- Parse.!!! Parse.sort))
  1213       >> Isar_Cmd.print_type);
  1214 
  1215 val _ =
  1216   Outer_Syntax.command \<^command_keyword>\<open>print_codesetup\<close> "print code generator setup"
  1217     (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
  1218 
  1219 val _ =
  1220   Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
  1221     "print current proof state (if present)"
  1222     (opt_modes >> (fn modes =>
  1223       Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
  1224 
  1225 val _ =
  1226   Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
  1227     (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ()))));
  1228 
  1229 in end\<close>
  1230 
  1231 
  1232 subsection \<open>Dependencies\<close>
  1233 
  1234 ML \<open>
  1235 local
  1236 
  1237 val theory_bounds =
  1238   Parse.position Parse.theory_name >> single ||
  1239   (\<^keyword>\<open>(\<close> |-- Parse.enum "|" (Parse.position Parse.theory_name) --| \<^keyword>\<open>)\<close>);
  1240 
  1241 val _ =
  1242   Outer_Syntax.command \<^command_keyword>\<open>thy_deps\<close> "visualize theory dependencies"
  1243     (Scan.option theory_bounds -- Scan.option theory_bounds >>
  1244       (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
  1245 
  1246 
  1247 val class_bounds =
  1248   Parse.sort >> single ||
  1249   (\<^keyword>\<open>(\<close> |-- Parse.enum "|" Parse.sort --| \<^keyword>\<open>)\<close>);
  1250 
  1251 val _ =
  1252   Outer_Syntax.command \<^command_keyword>\<open>class_deps\<close> "visualize class dependencies"
  1253     (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
  1254       Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
  1255 
  1256 
  1257 val _ =
  1258   Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close> "visualize theorem dependencies"
  1259     (Parse.thms1 >> (fn args =>
  1260       Toplevel.keep (fn st =>
  1261         Thm_Deps.thm_deps (Toplevel.theory_of st)
  1262           (Attrib.eval_thms (Toplevel.context_of st) args))));
  1263 
  1264 
  1265 val thy_names =
  1266   Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
  1267 
  1268 val _ =
  1269   Outer_Syntax.command \<^command_keyword>\<open>unused_thms\<close> "find unused theorems"
  1270     (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
  1271         Toplevel.keep (fn st =>
  1272           let
  1273             val thy = Toplevel.theory_of st;
  1274             val ctxt = Toplevel.context_of st;
  1275             fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
  1276             val check = Theory.check {long = false} ctxt;
  1277           in
  1278             Thm_Deps.unused_thms
  1279               (case opt_range of
  1280                 NONE => (Theory.parents_of thy, [thy])
  1281               | SOME (xs, NONE) => (map check xs, [thy])
  1282               | SOME (xs, SOME ys) => (map check xs, map check ys))
  1283             |> map pretty_thm |> Pretty.writeln_chunks
  1284           end)));
  1285 
  1286 in end\<close>
  1287 
  1288 
  1289 subsubsection \<open>Find consts and theorems\<close>
  1290 
  1291 ML \<open>
  1292 local
  1293 
  1294 val _ =
  1295   Outer_Syntax.command \<^command_keyword>\<open>find_consts\<close>
  1296     "find constants by name / type patterns"
  1297     (Find_Consts.query_parser >> (fn spec =>
  1298       Toplevel.keep (fn st =>
  1299         Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
  1300 
  1301 val options =
  1302   Scan.optional
  1303     (Parse.$$$ "(" |--
  1304       Parse.!!! (Scan.option Parse.nat --
  1305         Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
  1306     (NONE, true);
  1307 
  1308 val _ =
  1309   Outer_Syntax.command \<^command_keyword>\<open>find_theorems\<close>
  1310     "find theorems meeting specified criteria"
  1311     (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
  1312       Toplevel.keep (fn st =>
  1313         Pretty.writeln
  1314           (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
  1315 
  1316 in end\<close>
  1317 
  1318 
  1319 subsection \<open>Code generation\<close>
  1320 
  1321 ML \<open>
  1322 local
  1323 
  1324 val _ =
  1325   Outer_Syntax.command \<^command_keyword>\<open>code_datatype\<close>
  1326     "define set of code datatype constructors"
  1327     (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd));
  1328 
  1329 in end\<close>
  1330 
  1331 
  1332 subsection \<open>Extraction of programs from proofs\<close>
  1333 
  1334 ML \<open>
  1335 local
  1336 
  1337 val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
  1338 
  1339 val _ =
  1340   Outer_Syntax.command \<^command_keyword>\<open>realizers\<close>
  1341     "specify realizers for primitive axioms / theorems, together with correctness proof"
  1342     (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
  1343      (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
  1344        (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
  1345 
  1346 val _ =
  1347   Outer_Syntax.command \<^command_keyword>\<open>realizability\<close>
  1348     "add equations characterizing realizability"
  1349     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
  1350 
  1351 val _ =
  1352   Outer_Syntax.command \<^command_keyword>\<open>extract_type\<close>
  1353     "add equations characterizing type of extracted program"
  1354     (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
  1355 
  1356 val _ =
  1357   Outer_Syntax.command \<^command_keyword>\<open>extract\<close> "extract terms from proofs"
  1358     (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
  1359       Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
  1360 
  1361 in end\<close>
  1362 
  1363 
  1364 section \<open>Auxiliary lemmas\<close>
  1365 
  1366 subsection \<open>Meta-level connectives in assumptions\<close>
  1367 
  1368 lemma meta_mp:
  1369   assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
  1370   shows "PROP Q"
  1371     by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
  1372 
  1373 lemmas meta_impE = meta_mp [elim_format]
  1374 
  1375 lemma meta_spec:
  1376   assumes "\<And>x. PROP P x"
  1377   shows "PROP P x"
  1378     by (rule \<open>\<And>x. PROP P x\<close>)
  1379 
  1380 lemmas meta_allE = meta_spec [elim_format]
  1381 
  1382 lemma swap_params:
  1383   "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
  1384 
  1385 
  1386 subsection \<open>Meta-level conjunction\<close>
  1387 
  1388 lemma all_conjunction:
  1389   "(\<And>x. PROP A x &&& PROP B x) \<equiv> ((\<And>x. PROP A x) &&& (\<And>x. PROP B x))"
  1390 proof
  1391   assume conj: "\<And>x. PROP A x &&& PROP B x"
  1392   show "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1393   proof -
  1394     fix x
  1395     from conj show "PROP A x" by (rule conjunctionD1)
  1396     from conj show "PROP B x" by (rule conjunctionD2)
  1397   qed
  1398 next
  1399   assume conj: "(\<And>x. PROP A x) &&& (\<And>x. PROP B x)"
  1400   fix x
  1401   show "PROP A x &&& PROP B x"
  1402   proof -
  1403     show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
  1404     show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
  1405   qed
  1406 qed
  1407 
  1408 lemma imp_conjunction:
  1409   "(PROP A \<Longrightarrow> PROP B &&& PROP C) \<equiv> ((PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C))"
  1410 proof
  1411   assume conj: "PROP A \<Longrightarrow> PROP B &&& PROP C"
  1412   show "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1413   proof -
  1414     assume "PROP A"
  1415     from conj [OF \<open>PROP A\<close>] show "PROP B" by (rule conjunctionD1)
  1416     from conj [OF \<open>PROP A\<close>] show "PROP C" by (rule conjunctionD2)
  1417   qed
  1418 next
  1419   assume conj: "(PROP A \<Longrightarrow> PROP B) &&& (PROP A \<Longrightarrow> PROP C)"
  1420   assume "PROP A"
  1421   show "PROP B &&& PROP C"
  1422   proof -
  1423     from \<open>PROP A\<close> show "PROP B" by (rule conj [THEN conjunctionD1])
  1424     from \<open>PROP A\<close> show "PROP C" by (rule conj [THEN conjunctionD2])
  1425   qed
  1426 qed
  1427 
  1428 lemma conjunction_imp:
  1429   "(PROP A &&& PROP B \<Longrightarrow> PROP C) \<equiv> (PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C)"
  1430 proof
  1431   assume r: "PROP A &&& PROP B \<Longrightarrow> PROP C"
  1432   assume ab: "PROP A" "PROP B"
  1433   show "PROP C"
  1434   proof (rule r)
  1435     from ab show "PROP A &&& PROP B" .
  1436   qed
  1437 next
  1438   assume r: "PROP A \<Longrightarrow> PROP B \<Longrightarrow> PROP C"
  1439   assume conj: "PROP A &&& PROP B"
  1440   show "PROP C"
  1441   proof (rule r)
  1442     from conj show "PROP A" by (rule conjunctionD1)
  1443     from conj show "PROP B" by (rule conjunctionD2)
  1444   qed
  1445 qed
  1446 
  1447 declare [[ML_write_global = false]]
  1448 
  1449 end