src/Pure/ML/ml_thms.ML
author wenzelm
Thu, 21 Aug 2014 22:48:39 +0200
changeset 58028 e4250d370657
parent 58011 bc6bced136e5
child 58033 154ae20ead35
permissions -rw-r--r--
tuned signature -- define some elementary operations earlier;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_thms.ML
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     3
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
     4
Attribute source and theorem values within ML.
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     5
*)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     6
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     7
signature ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
     8
sig
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 56304
diff changeset
     9
  val the_attributes: Proof.context -> int -> Token.src list
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    10
  val the_thmss: Proof.context -> thm list list
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    11
  val get_stored_thms: unit -> thm list
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    12
  val get_stored_thm: unit -> thm
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    13
  val store_thms: string * thm list -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    14
  val store_thm: string * thm -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    15
  val bind_thm: string * thm -> unit
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
    16
  val bind_thms: string * thm list -> unit
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    17
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    18
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    19
structure ML_Thms: ML_THMS =
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    20
struct
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    21
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    22
(* auxiliary data *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    23
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    24
type thms = (string * bool) * thm list;  (*name, single, value*)
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    25
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    26
structure Data = Proof_Data
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    27
(
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 56304
diff changeset
    28
  type T = Token.src list Inttab.table * thms list;
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    29
  fun init _ = (Inttab.empty, []);
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    30
);
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    31
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    32
val put_attributes = Data.map o apfst o Inttab.update;
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    33
fun the_attributes ctxt name = the (Inttab.lookup (fst (Data.get ctxt)) name);
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    34
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    35
val get_thmss = snd o Data.get;
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    36
val the_thmss = map snd o get_thmss;
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    37
val cons_thms = Data.map o apsnd o cons;
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    38
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    39
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    40
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    41
(* attribute source *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    42
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    43
val _ = Theory.setup
58028
e4250d370657 tuned signature -- define some elementary operations earlier;
wenzelm
parents: 58011
diff changeset
    44
  (ML_Antiquotation.declaration @{binding attributes} (Scan.lift Parse.attribs)
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    45
    (fn _ => fn raw_srcs => fn ctxt =>
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    46
      let
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    47
        val i = serial ();
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55914
diff changeset
    48
        val srcs = map (Attrib.check_src ctxt) raw_srcs;
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    49
        val _ = map (Attrib.attribute ctxt) srcs;
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    50
        val (a, ctxt') = ctxt
56072
31e427387ab5 tuned signature -- clarified module name;
wenzelm
parents: 56069
diff changeset
    51
          |> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs);
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    52
        val ml =
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    53
          ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    54
            string_of_int i ^ ";\n", "Isabelle." ^ a);
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    55
      in (K ml, ctxt') end));
45592
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    56
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    57
8baa0b7f3f66 added ML antiquotation @{attributes};
wenzelm
parents: 45198
diff changeset
    58
(* fact references *)
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    59
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    60
fun thm_binding kind is_single thms ctxt =
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    61
  let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    62
    val initial = null (get_thmss ctxt);
56072
31e427387ab5 tuned signature -- clarified module name;
wenzelm
parents: 56069
diff changeset
    63
    val (name, ctxt') = ML_Antiquotation.variant kind ctxt;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    64
    val ctxt'' = cons_thms ((name, is_single), thms) ctxt';
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    65
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    66
    val ml_body = "Isabelle." ^ name;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    67
    fun decl final_ctxt =
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    68
      if initial then
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    69
        let
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
    70
          val binds = get_thmss final_ctxt |> map (fn ((a, b), _) => (b ? enclose "[" "]") a);
48782
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    71
          val ml_env = "val [" ^ commas binds ^ "] = ML_Thms.the_thmss ML_context;\n";
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    72
        in (ml_env, ml_body) end
e955964d89cb more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
wenzelm
parents: 48776
diff changeset
    73
      else ("", ml_body);
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    74
  in (decl, ctxt'') end;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    75
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    76
val _ = Theory.setup
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56199
diff changeset
    77
  (ML_Antiquotation.declaration @{binding thm} (Attrib.thm >> single) (K (thm_binding "thm" true)) #>
ceb8a93460b7 clarified modules;
wenzelm
parents: 56199
diff changeset
    78
   ML_Antiquotation.declaration @{binding thms} Attrib.thms (K (thm_binding "thms" false)));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    79
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    80
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    81
(* ad-hoc goals *)
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    82
30266
970bf4f594c9 ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
wenzelm
parents: 29606
diff changeset
    83
val and_ = Args.$$$ "and";
27809
a1e409db516b unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27521
diff changeset
    84
val by = Args.$$$ "by";
55111
5792f5106c40 tuned signature;
wenzelm
parents: 54883
diff changeset
    85
val goal = Scan.unless (by || and_) Args.name_inner_syntax;
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
    86
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53169
diff changeset
    87
val _ = Theory.setup
56205
ceb8a93460b7 clarified modules;
wenzelm
parents: 56199
diff changeset
    88
  (ML_Antiquotation.declaration @{binding lemma}
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    89
    (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) --
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    90
      (by |-- Method.parse -- Scan.option Method.parse)))
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    91
    (fn _ => fn ((is_open, raw_propss), (m1, m2)) => fn ctxt =>
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    92
      let
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    93
        val _ = Context_Position.reports ctxt (maps Method.reports_of (m1 :: the_list m2));
55515
0e161deca64d more markup;
wenzelm
parents: 55111
diff changeset
    94
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    95
        val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    96
        val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation;
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    97
        fun after_qed res goal_ctxt =
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    98
          Proof_Context.put_thms false (Auto_Bind.thisN,
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
    99
            SOME (map prep_result (Proof_Context.export goal_ctxt ctxt (flat res)))) goal_ctxt;
53169
e2d31807cbf6 clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents: 53168
diff changeset
   100
56069
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   101
        val ctxt' = ctxt
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   102
          |> Proof.theorem NONE after_qed propss
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   103
          |> Proof.global_terminal_proof (m1, m2);
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   104
        val thms =
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   105
          Proof_Context.get_fact ctxt'
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   106
            (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
451d5b73f8cf simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
wenzelm
parents: 55997
diff changeset
   107
      in thm_binding "lemma" (length (flat propss) = 1) thms ctxt end));
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   108
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   109
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   110
(* old-style theorem bindings *)
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   111
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   112
structure Stored_Thms = Theory_Data
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   113
(
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   114
  type T = thm list;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   115
  val empty = [];
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   116
  fun extend _ = [];
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   117
  fun merge _ = [];
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   118
);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   119
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   120
fun get_stored_thms () = Stored_Thms.get (ML_Context.the_global_context ());
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   121
val get_stored_thm = hd o get_stored_thms;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   122
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   123
fun ml_store get (name, ths) =
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   124
  let
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   125
    val ths' = Context.>>> (Context.map_theory_result
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   126
      (Global_Theory.store_thms (Binding.name name, ths)));
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   127
    val _ = Theory.setup (Stored_Thms.put ths');
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   128
    val _ =
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   129
      if name = "" then ()
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   130
      else if not (ML_Syntax.is_identifier name) then
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   131
        error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   132
      else
56304
40274e4f5ebf redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents: 56275
diff changeset
   133
        ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
56199
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   134
          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   135
    val _ = Theory.setup (Stored_Thms.put []);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   136
  in () end;
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   137
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   138
val store_thms = ml_store "ML_Thms.get_stored_thms";
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   139
fun store_thm (name, th) = ml_store "ML_Thms.get_stored_thm" (name, [th]);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   140
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   141
fun bind_thm (name, thm) = store_thm (name, Drule.export_without_context thm);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   142
fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);
8e8d28ed7529 tuned signature -- rearranged modules;
wenzelm
parents: 56072
diff changeset
   143
27389
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   144
end;
823c7ec3ea4f Isar theorem values within ML.
wenzelm
parents:
diff changeset
   145