src/Pure/Pure.thy
changeset 62856 3f97aa4580c6
parent 62849 caaa2fc4040d
child 62859 b2f951051472
     1.1 --- a/src/Pure/Pure.thy	Mon Apr 04 20:46:39 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Mon Apr 04 22:13:08 2016 +0200
     1.3 @@ -95,191 +95,9 @@
     1.4  
     1.5  section \<open>Isar commands\<close>
     1.6  
     1.7 -ML \<open>
     1.8 -local
     1.9 -
    1.10 -(** theory commands **)
    1.11 -
    1.12 -(* sorts *)
    1.13 -
    1.14 -val _ =
    1.15 -  Outer_Syntax.local_theory @{command_keyword default_sort}
    1.16 -    "declare default sort for explicit type variables"
    1.17 -    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
    1.18 -
    1.19 -
    1.20 -(* types *)
    1.21 -
    1.22 -val _ =
    1.23 -  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
    1.24 -    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
    1.25 -      >> (fn ((args, a), mx) =>
    1.26 -          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
    1.27 -
    1.28 -val _ =
    1.29 -  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
    1.30 -    (Parse.type_args -- Parse.binding --
    1.31 -      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
    1.32 -      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
    1.33 -
    1.34 -val _ =
    1.35 -  Outer_Syntax.command @{command_keyword nonterminal}
    1.36 -    "declare syntactic type constructors (grammar nonterminal symbols)"
    1.37 -    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
    1.38 -
    1.39 -
    1.40 -(* consts and syntax *)
    1.41 -
    1.42 -val _ =
    1.43 -  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
    1.44 -    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
    1.45 -
    1.46 -val _ =
    1.47 -  Outer_Syntax.command @{command_keyword consts} "declare constants"
    1.48 -    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
    1.49 -
    1.50 -val mode_spec =
    1.51 -  (@{keyword "output"} >> K ("", false)) ||
    1.52 -    Parse.name -- Scan.optional (@{keyword "output"} >> K false) true;
    1.53 -
    1.54 -val opt_mode =
    1.55 -  Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
    1.56 -
    1.57 -val _ =
    1.58 -  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
    1.59 -    (opt_mode -- Scan.repeat1 Parse.const_decl
    1.60 -      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
    1.61 -
    1.62 -val _ =
    1.63 -  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
    1.64 -    (opt_mode -- Scan.repeat1 Parse.const_decl
    1.65 -      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
    1.66 -
    1.67 -
    1.68 -(* translations *)
    1.69 -
    1.70 -val trans_pat =
    1.71 -  Scan.optional
    1.72 -    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
    1.73 -    -- Parse.inner_syntax Parse.string;
    1.74 -
    1.75 -fun trans_arrow toks =
    1.76 -  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
    1.77 -    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
    1.78 -    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
    1.79 -
    1.80 -val trans_line =
    1.81 -  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
    1.82 -    >> (fn (left, (arr, right)) => arr (left, right));
    1.83 -
    1.84 -val _ =
    1.85 -  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
    1.86 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
    1.87 -
    1.88 -val _ =
    1.89 -  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
    1.90 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
    1.91 -
    1.92 -
    1.93 -(* constant definitions and abbreviations *)
    1.94 -
    1.95 -val _ =
    1.96 -  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
    1.97 -    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
    1.98 +subsection \<open>Embedded ML text\<close>
    1.99  
   1.100 -val _ =
   1.101 -  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   1.102 -    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   1.103 -      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   1.104 -
   1.105 -val _ =
   1.106 -  Outer_Syntax.local_theory @{command_keyword type_notation}
   1.107 -    "add concrete syntax for type constructors"
   1.108 -    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   1.109 -      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   1.110 -
   1.111 -val _ =
   1.112 -  Outer_Syntax.local_theory @{command_keyword no_type_notation}
   1.113 -    "delete concrete syntax for type constructors"
   1.114 -    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   1.115 -      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   1.116 -
   1.117 -val _ =
   1.118 -  Outer_Syntax.local_theory @{command_keyword notation}
   1.119 -    "add concrete syntax for constants / fixed variables"
   1.120 -    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   1.121 -      >> (fn (mode, args) => Specification.notation_cmd true mode args));
   1.122 -
   1.123 -val _ =
   1.124 -  Outer_Syntax.local_theory @{command_keyword no_notation}
   1.125 -    "delete concrete syntax for constants / fixed variables"
   1.126 -    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   1.127 -      >> (fn (mode, args) => Specification.notation_cmd false mode args));
   1.128 -
   1.129 -
   1.130 -(* constant specifications *)
   1.131 -
   1.132 -val _ =
   1.133 -  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
   1.134 -    (Scan.optional Parse.fixes [] --
   1.135 -      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
   1.136 -      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   1.137 -
   1.138 -
   1.139 -(* theorems *)
   1.140 -
   1.141 -val _ =
   1.142 -  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
   1.143 -    (Parse_Spec.name_facts -- Parse.for_fixes >>
   1.144 -      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
   1.145 -
   1.146 -val _ =
   1.147 -  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   1.148 -    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
   1.149 -      >> (fn (facts, fixes) =>
   1.150 -          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
   1.151 -
   1.152 -val _ =
   1.153 -  Outer_Syntax.local_theory @{command_keyword named_theorems}
   1.154 -    "declare named collection of theorems"
   1.155 -    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   1.156 -      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
   1.157 -
   1.158 -
   1.159 -(* hide names *)
   1.160 -
   1.161 -local
   1.162 -
   1.163 -fun hide_names command_keyword what hide parse prep =
   1.164 -  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
   1.165 -    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
   1.166 -      (Toplevel.theory (fn thy =>
   1.167 -        let val ctxt = Proof_Context.init_global thy
   1.168 -        in fold (hide fully o prep ctxt) args thy end))));
   1.169 -
   1.170 -in
   1.171 -
   1.172 -val _ =
   1.173 -  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
   1.174 -    Proof_Context.read_class;
   1.175 -
   1.176 -val _ =
   1.177 -  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
   1.178 -    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
   1.179 -
   1.180 -val _ =
   1.181 -  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
   1.182 -    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
   1.183 -
   1.184 -val _ =
   1.185 -  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
   1.186 -    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
   1.187 -
   1.188 -end;
   1.189 -
   1.190 -
   1.191 -(* use ML text *)
   1.192 -
   1.193 +ML \<open>
   1.194  local
   1.195  
   1.196  fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
   1.197 @@ -309,8 +127,6 @@
   1.198        (ML_Context.exec (fn () => ML_Context.eval_source flags source))
   1.199    end);
   1.200  
   1.201 -in
   1.202 -
   1.203  val _ =
   1.204    Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
   1.205      (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
   1.206 @@ -339,8 +155,6 @@
   1.207      "read and evaluate Standard ML file (no debugger information)"
   1.208      (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false));
   1.209  
   1.210 -end;
   1.211 -
   1.212  val _ =
   1.213    Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
   1.214      (Parse.ML_source >> (fn source =>
   1.215 @@ -391,6 +205,11 @@
   1.216      (Parse.ML_source >> Isar_Cmd.local_setup);
   1.217  
   1.218  val _ =
   1.219 +  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
   1.220 +    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
   1.221 +      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
   1.222 +
   1.223 +val _ =
   1.224    Outer_Syntax.local_theory @{command_keyword attribute_setup} "define attribute in ML"
   1.225      (Parse.position Parse.name --
   1.226          Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
   1.227 @@ -419,8 +238,101 @@
   1.228        Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
   1.229      >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
   1.230  
   1.231 +in end\<close>
   1.232  
   1.233 -(* translation functions *)
   1.234 +
   1.235 +subsection \<open>Theory commands\<close>
   1.236 +
   1.237 +subsubsection \<open>Sorts and types\<close>
   1.238 +
   1.239 +ML \<open>
   1.240 +local
   1.241 +
   1.242 +val _ =
   1.243 +  Outer_Syntax.local_theory @{command_keyword default_sort}
   1.244 +    "declare default sort for explicit type variables"
   1.245 +    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
   1.246 +
   1.247 +val _ =
   1.248 +  Outer_Syntax.local_theory @{command_keyword typedecl} "type declaration"
   1.249 +    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
   1.250 +      >> (fn ((args, a), mx) =>
   1.251 +          Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd));
   1.252 +
   1.253 +val _ =
   1.254 +  Outer_Syntax.local_theory @{command_keyword type_synonym} "declare type abbreviation"
   1.255 +    (Parse.type_args -- Parse.binding --
   1.256 +      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
   1.257 +      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
   1.258 +
   1.259 +in end\<close>
   1.260 +
   1.261 +
   1.262 +subsubsection \<open>Consts\<close>
   1.263 +
   1.264 +ML \<open>
   1.265 +local
   1.266 +
   1.267 +val _ =
   1.268 +  Outer_Syntax.command @{command_keyword judgment} "declare object-logic judgment"
   1.269 +    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   1.270 +
   1.271 +val _ =
   1.272 +  Outer_Syntax.command @{command_keyword consts} "declare constants"
   1.273 +    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd));
   1.274 +
   1.275 +in end\<close>
   1.276 +
   1.277 +
   1.278 +subsubsection \<open>Syntax and translations\<close>
   1.279 +
   1.280 +ML \<open>
   1.281 +local
   1.282 +
   1.283 +val _ =
   1.284 +  Outer_Syntax.command @{command_keyword nonterminal}
   1.285 +    "declare syntactic type constructors (grammar nonterminal symbols)"
   1.286 +    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
   1.287 +
   1.288 +val _ =
   1.289 +  Outer_Syntax.command @{command_keyword syntax} "add raw syntax clauses"
   1.290 +    (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
   1.291 +      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
   1.292 +
   1.293 +val _ =
   1.294 +  Outer_Syntax.command @{command_keyword no_syntax} "delete raw syntax clauses"
   1.295 +    (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
   1.296 +      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
   1.297 +
   1.298 +val trans_pat =
   1.299 +  Scan.optional
   1.300 +    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
   1.301 +    -- Parse.inner_syntax Parse.string;
   1.302 +
   1.303 +fun trans_arrow toks =
   1.304 +  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
   1.305 +    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
   1.306 +    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
   1.307 +
   1.308 +val trans_line =
   1.309 +  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
   1.310 +    >> (fn (left, (arr, right)) => arr (left, right));
   1.311 +
   1.312 +val _ =
   1.313 +  Outer_Syntax.command @{command_keyword translations} "add syntax translation rules"
   1.314 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
   1.315 +
   1.316 +val _ =
   1.317 +  Outer_Syntax.command @{command_keyword no_translations} "delete syntax translation rules"
   1.318 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
   1.319 +
   1.320 +in end\<close>
   1.321 +
   1.322 +
   1.323 +subsubsection \<open>Translation functions\<close>
   1.324 +
   1.325 +ML \<open>
   1.326 +local
   1.327  
   1.328  val _ =
   1.329    Outer_Syntax.command @{command_keyword parse_ast_translation}
   1.330 @@ -447,16 +359,124 @@
   1.331      "install print ast translation functions"
   1.332      (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
   1.333  
   1.334 +in end\<close>
   1.335  
   1.336 -(* oracles *)
   1.337 +
   1.338 +subsubsection \<open>Specifications\<close>
   1.339 +
   1.340 +ML \<open>
   1.341 +local
   1.342 +
   1.343 +val _ =
   1.344 +  Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
   1.345 +    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
   1.346 +
   1.347 +val _ =
   1.348 +  Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
   1.349 +    (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
   1.350 +      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
   1.351 +
   1.352 +val _ =
   1.353 +  Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
   1.354 +    (Scan.optional Parse.fixes [] --
   1.355 +      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
   1.356 +      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
   1.357 +
   1.358 +in end\<close>
   1.359 +
   1.360 +
   1.361 +subsubsection \<open>Notation\<close>
   1.362 +
   1.363 +ML \<open>
   1.364 +local
   1.365 +
   1.366 +val _ =
   1.367 +  Outer_Syntax.local_theory @{command_keyword type_notation}
   1.368 +    "add concrete syntax for type constructors"
   1.369 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   1.370 +      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
   1.371 +
   1.372 +val _ =
   1.373 +  Outer_Syntax.local_theory @{command_keyword no_type_notation}
   1.374 +    "delete concrete syntax for type constructors"
   1.375 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
   1.376 +      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
   1.377 +
   1.378 +val _ =
   1.379 +  Outer_Syntax.local_theory @{command_keyword notation}
   1.380 +    "add concrete syntax for constants / fixed variables"
   1.381 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   1.382 +      >> (fn (mode, args) => Specification.notation_cmd true mode args));
   1.383  
   1.384  val _ =
   1.385 -  Outer_Syntax.command @{command_keyword oracle} "declare oracle"
   1.386 -    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
   1.387 -      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
   1.388 +  Outer_Syntax.local_theory @{command_keyword no_notation}
   1.389 +    "delete concrete syntax for constants / fixed variables"
   1.390 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   1.391 +      >> (fn (mode, args) => Specification.notation_cmd false mode args));
   1.392 +
   1.393 +in end\<close>
   1.394 +
   1.395 +
   1.396 +subsubsection \<open>Theorems\<close>
   1.397 +
   1.398 +ML \<open>
   1.399 +local
   1.400 +
   1.401 +val _ =
   1.402 +  Outer_Syntax.local_theory' @{command_keyword lemmas} "define theorems"
   1.403 +    (Parse_Spec.name_facts -- Parse.for_fixes >>
   1.404 +      (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes));
   1.405 +
   1.406 +val _ =
   1.407 +  Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems"
   1.408 +    (Parse.and_list1 Parse.xthms1 -- Parse.for_fixes
   1.409 +      >> (fn (facts, fixes) =>
   1.410 +          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
   1.411 +
   1.412 +val _ =
   1.413 +  Outer_Syntax.local_theory @{command_keyword named_theorems}
   1.414 +    "declare named collection of theorems"
   1.415 +    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
   1.416 +      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
   1.417 +
   1.418 +in end\<close>
   1.419  
   1.420  
   1.421 -(* bundled declarations *)
   1.422 +subsubsection \<open>Hide names\<close>
   1.423 +
   1.424 +ML \<open>
   1.425 +local
   1.426 +
   1.427 +fun hide_names command_keyword what hide parse prep =
   1.428 +  Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space")
   1.429 +    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) =>
   1.430 +      (Toplevel.theory (fn thy =>
   1.431 +        let val ctxt = Proof_Context.init_global thy
   1.432 +        in fold (hide fully o prep ctxt) args thy end))));
   1.433 +
   1.434 +val _ =
   1.435 +  hide_names @{command_keyword hide_class} "classes" Sign.hide_class Parse.class
   1.436 +    Proof_Context.read_class;
   1.437 +
   1.438 +val _ =
   1.439 +  hide_names @{command_keyword hide_type} "types" Sign.hide_type Parse.type_const
   1.440 +    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false});
   1.441 +
   1.442 +val _ =
   1.443 +  hide_names @{command_keyword hide_const} "consts" Sign.hide_const Parse.const
   1.444 +    ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false});
   1.445 +
   1.446 +val _ =
   1.447 +  hide_names @{command_keyword hide_fact} "facts" Global_Theory.hide_fact
   1.448 +    (Parse.position Parse.xname) (Global_Theory.check_fact o Proof_Context.theory_of);
   1.449 +
   1.450 +in end\<close>
   1.451 +
   1.452 +
   1.453 +subsection \<open>Bundled declarations\<close>
   1.454 +
   1.455 +ML \<open>
   1.456 +local
   1.457  
   1.458  val _ =
   1.459    Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
   1.460 @@ -478,8 +498,15 @@
   1.461      "print bundles of declarations"
   1.462      (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
   1.463  
   1.464 +in end\<close>
   1.465  
   1.466 -(* local theories *)
   1.467 +
   1.468 +subsection \<open>Local theory specifications\<close>
   1.469 +
   1.470 +subsubsection \<open>Specification context\<close>
   1.471 +
   1.472 +ML \<open>
   1.473 +local
   1.474  
   1.475  val _ =
   1.476    Outer_Syntax.command @{command_keyword context} "begin local theory context"
   1.477 @@ -489,8 +516,19 @@
   1.478          >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
   1.479        --| Parse.begin);
   1.480  
   1.481 +val _ =
   1.482 +  Outer_Syntax.command @{command_keyword end} "end context"
   1.483 +    (Scan.succeed
   1.484 +      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
   1.485 +        Toplevel.end_proof (K Proof.end_notepad)));
   1.486  
   1.487 -(* locales *)
   1.488 +in end\<close>
   1.489 +
   1.490 +
   1.491 +subsubsection \<open>Locales and interpretation\<close>
   1.492 +
   1.493 +ML \<open>
   1.494 +local
   1.495  
   1.496  val locale_val =
   1.497    Parse_Spec.locale_expression --
   1.498 @@ -532,8 +570,8 @@
   1.499  val _ =
   1.500    Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
   1.501      "prove interpretation of locale expression into global theory"
   1.502 -    (interpretation_args_with_defs
   1.503 -      >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations));
   1.504 +    (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
   1.505 +      Interpretation.global_interpretation_cmd expr defs equations));
   1.506  
   1.507  val _ =
   1.508    Outer_Syntax.command @{command_keyword sublocale}
   1.509 @@ -548,11 +586,16 @@
   1.510    Outer_Syntax.command @{command_keyword interpretation}
   1.511      "prove interpretation of locale expression in local theory or into global theory"
   1.512      (interpretation_args >> (fn (expr, equations) =>
   1.513 -      Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations)));
   1.514 +      Toplevel.local_theory_to_proof NONE NONE
   1.515 +        (Interpretation.isar_interpretation_cmd expr equations)));
   1.516 +
   1.517 +in end\<close>
   1.518  
   1.519  
   1.520 +subsubsection \<open>Type classes\<close>
   1.521  
   1.522 -(* classes *)
   1.523 +ML \<open>
   1.524 +local
   1.525  
   1.526  val class_val =
   1.527    Parse_Spec.class_expression --
   1.528 @@ -582,8 +625,13 @@
   1.529      Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof ||
   1.530      Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I)));
   1.531  
   1.532 +in end\<close>
   1.533  
   1.534 -(* arbitrary overloading *)
   1.535 +
   1.536 +subsubsection \<open>Arbitrary overloading\<close>
   1.537 +
   1.538 +ML \<open>
   1.539 +local
   1.540  
   1.541  val _ =
   1.542    Outer_Syntax.command @{command_keyword overloading} "overloaded definitions"
   1.543 @@ -592,34 +640,30 @@
   1.544        >> Scan.triple1) --| Parse.begin
   1.545     >> (fn operations => Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
   1.546  
   1.547 -
   1.548 -(* code generation *)
   1.549 -
   1.550 -val _ =
   1.551 -  Outer_Syntax.command @{command_keyword code_datatype}
   1.552 -    "define set of code datatype constructors"
   1.553 -    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
   1.554 +in end\<close>
   1.555  
   1.556  
   1.557 +subsection \<open>Proof commands\<close>
   1.558  
   1.559 -(** proof commands **)
   1.560 +ML \<open>
   1.561 +local
   1.562  
   1.563  val _ =
   1.564    Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
   1.565      (Parse.begin >> K Proof.begin_notepad);
   1.566  
   1.567 +in end\<close>
   1.568  
   1.569 -(* statements *)
   1.570 +
   1.571 +subsubsection \<open>Statements\<close>
   1.572 +
   1.573 +ML \<open>
   1.574 +local
   1.575  
   1.576  val structured_statement =
   1.577    Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes
   1.578      >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows));
   1.579  
   1.580 -val structured_statement' =
   1.581 -  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
   1.582 -    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   1.583 -
   1.584 -
   1.585  fun theorem spec schematic descr =
   1.586    Outer_Syntax.local_theory_to_proof' spec
   1.587      ("state " ^ descr)
   1.588 @@ -658,8 +702,13 @@
   1.589      (structured_statement >> (fn (a, b, c, d) =>
   1.590        Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2)));
   1.591  
   1.592 +in end\<close>
   1.593  
   1.594 -(* facts *)
   1.595 +
   1.596 +subsubsection \<open>Local facts\<close>
   1.597 +
   1.598 +ML \<open>
   1.599 +local
   1.600  
   1.601  val facts = Parse.and_list1 Parse.xthms1;
   1.602  
   1.603 @@ -691,8 +740,17 @@
   1.604    Outer_Syntax.command @{command_keyword unfolding} "unfold definitions in goal and facts"
   1.605      (facts >> (Toplevel.proof o Proof.unfolding_cmd));
   1.606  
   1.607 +in end\<close>
   1.608  
   1.609 -(* proof context *)
   1.610 +
   1.611 +subsubsection \<open>Proof context\<close>
   1.612 +
   1.613 +ML \<open>
   1.614 +local
   1.615 +
   1.616 +val structured_statement =
   1.617 +  Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes
   1.618 +    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   1.619  
   1.620  val _ =
   1.621    Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
   1.622 @@ -700,11 +758,11 @@
   1.623  
   1.624  val _ =
   1.625    Outer_Syntax.command @{command_keyword assume} "assume propositions"
   1.626 -    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
   1.627 +    (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c)));
   1.628  
   1.629  val _ =
   1.630    Outer_Syntax.command @{command_keyword presume} "assume propositions, to be established later"
   1.631 -    (structured_statement' >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
   1.632 +    (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c)));
   1.633  
   1.634  val _ =
   1.635    Outer_Syntax.command @{command_keyword def} "local definition (non-polymorphic)"
   1.636 @@ -734,7 +792,7 @@
   1.637  
   1.638  val _ =
   1.639    Outer_Syntax.command @{command_keyword write} "add concrete syntax for constants / fixed variables"
   1.640 -    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   1.641 +    (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
   1.642      >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args)));
   1.643  
   1.644  val _ =
   1.645 @@ -745,8 +803,13 @@
   1.646            --| @{keyword ")"}) ||
   1.647          Parse.position Parse.xname >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
   1.648  
   1.649 +in end\<close>
   1.650  
   1.651 -(* proof structure *)
   1.652 +
   1.653 +subsubsection \<open>Proof structure\<close>
   1.654 +
   1.655 +ML \<open>
   1.656 +local
   1.657  
   1.658  val _ =
   1.659    Outer_Syntax.command @{command_keyword "{"} "begin explicit proof block"
   1.660 @@ -760,8 +823,13 @@
   1.661    Outer_Syntax.command @{command_keyword next} "enter next proof block"
   1.662      (Scan.succeed (Toplevel.proof Proof.next_block));
   1.663  
   1.664 +in end\<close>
   1.665  
   1.666 -(* end proof *)
   1.667 +
   1.668 +subsubsection \<open>End proof\<close>
   1.669 +
   1.670 +ML \<open>
   1.671 +local
   1.672  
   1.673  val _ =
   1.674    Outer_Syntax.command @{command_keyword qed} "conclude proof"
   1.675 @@ -800,8 +868,13 @@
   1.676    Outer_Syntax.command @{command_keyword oops} "forget proof"
   1.677      (Scan.succeed (Toplevel.forget_proof true));
   1.678  
   1.679 +in end\<close>
   1.680  
   1.681 -(* proof steps *)
   1.682 +
   1.683 +subsubsection \<open>Proof steps\<close>
   1.684 +
   1.685 +ML \<open>
   1.686 +local
   1.687  
   1.688  val _ =
   1.689    Outer_Syntax.command @{command_keyword defer} "shuffle internal proof state"
   1.690 @@ -824,9 +897,12 @@
   1.691      (Scan.option Method.parse >> (fn m =>
   1.692        (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
   1.693  
   1.694 +in end\<close>
   1.695  
   1.696 -(* subgoal focus *)
   1.697  
   1.698 +subsubsection \<open>Subgoal focus\<close>
   1.699 +
   1.700 +ML \<open>
   1.701  local
   1.702  
   1.703  val opt_fact_binding =
   1.704 @@ -840,8 +916,6 @@
   1.705          (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
   1.706      (false, []);
   1.707  
   1.708 -in
   1.709 -
   1.710  val _ =
   1.711    Outer_Syntax.command @{command_keyword subgoal}
   1.712      "focus on first subgoal within backward refinement"
   1.713 @@ -849,10 +923,13 @@
   1.714        for_params >> (fn ((a, b), c) =>
   1.715          Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
   1.716  
   1.717 -end;
   1.718 +in end\<close>
   1.719  
   1.720  
   1.721 -(* calculation *)
   1.722 +subsubsection \<open>Calculation\<close>
   1.723 +
   1.724 +ML \<open>
   1.725 +local
   1.726  
   1.727  val calculation_args =
   1.728    Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
   1.729 @@ -879,8 +956,13 @@
   1.730    Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
   1.731      (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
   1.732  
   1.733 +in end\<close>
   1.734  
   1.735 -(* proof navigation *)
   1.736 +
   1.737 +subsubsection \<open>Proof navigation\<close>
   1.738 +
   1.739 +ML \<open>
   1.740 +local
   1.741  
   1.742  fun report_back () =
   1.743    Output.report [Markup.markup Markup.bad "Explicit backtracking"];
   1.744 @@ -891,9 +973,13 @@
   1.745       (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
   1.746        Toplevel.skip_proof report_back));
   1.747  
   1.748 +in end\<close>
   1.749  
   1.750  
   1.751 -(** diagnostic commands (for interactive mode only) **)
   1.752 +subsection \<open>Diagnostic commands (for interactive mode only)\<close>
   1.753 +
   1.754 +ML \<open>
   1.755 +local
   1.756  
   1.757  val opt_modes =
   1.758    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
   1.759 @@ -1087,34 +1173,33 @@
   1.760      (Scan.repeat1 Parse.path >> (fn names =>
   1.761        Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
   1.762  
   1.763 +in end\<close>
   1.764  
   1.765 -(* deps *)
   1.766  
   1.767 +subsection \<open>Dependencies\<close>
   1.768 +
   1.769 +ML \<open>
   1.770  local
   1.771 -  val theory_bounds =
   1.772 -    Parse.position Parse.theory_xname >> single ||
   1.773 -    (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
   1.774 -in
   1.775 +
   1.776 +val theory_bounds =
   1.777 +  Parse.position Parse.theory_xname >> single ||
   1.778 +  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
   1.779  
   1.780  val _ =
   1.781    Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
   1.782      (Scan.option theory_bounds -- Scan.option theory_bounds >>
   1.783        (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
   1.784  
   1.785 -end;
   1.786  
   1.787 -local
   1.788 -  val class_bounds =
   1.789 -    Parse.sort >> single ||
   1.790 -    (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
   1.791 -in
   1.792 +val class_bounds =
   1.793 +  Parse.sort >> single ||
   1.794 +  (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
   1.795  
   1.796  val _ =
   1.797    Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
   1.798      (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
   1.799        Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
   1.800  
   1.801 -end;
   1.802  
   1.803  val _ =
   1.804    Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
   1.805 @@ -1123,10 +1208,9 @@
   1.806          Thm_Deps.thm_deps (Toplevel.theory_of st)
   1.807            (Attrib.eval_thms (Toplevel.context_of st) args))));
   1.808  
   1.809 -local
   1.810 -  val thy_names =
   1.811 -    Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
   1.812 -in
   1.813 +
   1.814 +val thy_names =
   1.815 +  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
   1.816  
   1.817  val _ =
   1.818    Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
   1.819 @@ -1146,10 +1230,13 @@
   1.820              |> map pretty_thm |> Pretty.writeln_chunks
   1.821            end)));
   1.822  
   1.823 -end;
   1.824 +in end\<close>
   1.825  
   1.826  
   1.827 -(* find *)
   1.828 +subsubsection \<open>Find consts and theorems\<close>
   1.829 +
   1.830 +ML \<open>
   1.831 +local
   1.832  
   1.833  val _ =
   1.834    Outer_Syntax.command @{command_keyword find_consts}
   1.835 @@ -1158,14 +1245,12 @@
   1.836        Toplevel.keep (fn st =>
   1.837          Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
   1.838  
   1.839 -local
   1.840 -  val options =
   1.841 -    Scan.optional
   1.842 -      (Parse.$$$ "(" |--
   1.843 -        Parse.!!! (Scan.option Parse.nat --
   1.844 -          Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
   1.845 -      (NONE, true);
   1.846 -in
   1.847 +val options =
   1.848 +  Scan.optional
   1.849 +    (Parse.$$$ "(" |--
   1.850 +      Parse.!!! (Scan.option Parse.nat --
   1.851 +        Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
   1.852 +    (NONE, true);
   1.853  
   1.854  val _ =
   1.855    Outer_Syntax.command @{command_keyword find_theorems}
   1.856 @@ -1175,11 +1260,26 @@
   1.857          Pretty.writeln
   1.858            (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
   1.859  
   1.860 -end;
   1.861 +in end\<close>
   1.862  
   1.863  
   1.864 +subsection \<open>Code generation\<close>
   1.865  
   1.866 -(** extraction of programs from proofs **)
   1.867 +ML \<open>
   1.868 +local
   1.869 +
   1.870 +val _ =
   1.871 +  Outer_Syntax.command @{command_keyword code_datatype}
   1.872 +    "define set of code datatype constructors"
   1.873 +    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
   1.874 +
   1.875 +in end\<close>
   1.876 +
   1.877 +
   1.878 +subsection \<open>Extraction of programs from proofs\<close>
   1.879 +
   1.880 +ML \<open>
   1.881 +local
   1.882  
   1.883  val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
   1.884  
   1.885 @@ -1205,21 +1305,10 @@
   1.886      (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
   1.887        Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
   1.888  
   1.889 +in end\<close>
   1.890  
   1.891  
   1.892 -(** end **)
   1.893 -
   1.894 -val _ =
   1.895 -  Outer_Syntax.command @{command_keyword end} "end context"
   1.896 -    (Scan.succeed
   1.897 -      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
   1.898 -        Toplevel.end_proof (K Proof.end_notepad)));
   1.899 -
   1.900 -in end;
   1.901 -\<close>
   1.902 -
   1.903 -
   1.904 -section \<open>Basic attributes\<close>
   1.905 +section \<open>Isar attributes\<close>
   1.906  
   1.907  attribute_setup tagged =
   1.908    \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>