src/HOL/Import/import_data.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47258 880e587eee9f
child 50214 67fb9a168d10
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47258
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     1
(*  Title:      HOL/Import/import_data.ML
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk, University of Innsbruck
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     3
    Author:     Alexander Krauss, QAware GmbH
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     4
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     5
Importer data.
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     6
*)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     7
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     8
signature IMPORT_DATA =
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
     9
sig
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    10
  val get_const_map : string -> theory -> string option
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    11
  val get_typ_map : string -> theory -> string option
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    12
  val get_const_def : string -> theory -> thm option
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    13
  val get_typ_def : string -> theory -> thm option
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    14
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    15
  val add_const_map : string -> string -> theory -> theory
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    16
  val add_typ_map : string -> string -> theory -> theory
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    17
  val add_const_def : string -> thm -> string option -> theory -> theory
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    18
  val add_typ_def : string -> string -> string -> thm -> theory -> theory
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    19
end
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    20
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    21
structure Import_Data: IMPORT_DATA =
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    22
struct
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    23
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    24
structure Data = Theory_Data
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    25
(
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    26
  type T = {const_map: string Symtab.table, ty_map: string Symtab.table,
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    27
            const_def: thm Symtab.table, ty_def: thm Symtab.table}
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    28
  val empty = {const_map = Symtab.empty, ty_map = Symtab.empty,
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    29
               const_def = Symtab.empty, ty_def = Symtab.empty}
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    30
  val extend = I
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    31
  fun merge
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    32
   ({const_map = cm1, ty_map = tm1, const_def = cd1, ty_def = td1},
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    33
    {const_map = cm2, ty_map = tm2, const_def = cd2, ty_def = td2}) : T =
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    34
    {const_map = Symtab.merge (K true) (cm1, cm2), ty_map = Symtab.merge (K true) (tm1, tm2),
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    35
     const_def = Symtab.merge (K true) (cd1, cd2), ty_def = Symtab.merge (K true) (td1, td2)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    36
    }
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    37
)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    38
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    39
fun get_const_map s thy = Symtab.lookup (#const_map (Data.get thy)) s
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    40
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    41
fun get_typ_map s thy = Symtab.lookup (#ty_map (Data.get thy)) s
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    42
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    43
fun get_const_def s thy = Symtab.lookup (#const_def (Data.get thy)) s
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    44
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    45
fun get_typ_def s thy = Symtab.lookup (#ty_def (Data.get thy)) s
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    46
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    47
fun add_const_map s1 s2 thy =
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    48
  Data.map (fn {const_map, ty_map, const_def, ty_def} =>
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    49
    {const_map = (Symtab.update (s1, s2) const_map), ty_map = ty_map,
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    50
     const_def = const_def, ty_def = ty_def}) thy
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    51
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    52
fun add_typ_map s1 s2 thy =
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    53
  Data.map (fn {const_map, ty_map, const_def, ty_def} =>
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    54
    {const_map = const_map, ty_map = (Symtab.update (s1, s2) ty_map),
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    55
     const_def = const_def, ty_def = ty_def}) thy
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    56
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    57
fun add_const_def s th name_opt thy =
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    58
  let
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    59
    val th = Thm.legacy_freezeT th
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    60
    val name = case name_opt of
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    61
         NONE => (fst o dest_Const o fst o HOLogic.dest_eq o
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    62
           HOLogic.dest_Trueprop o prop_of) th
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    63
       | SOME n => n
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    64
    val thy' = add_const_map s name thy
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    65
  in
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    66
    Data.map (fn {const_map, ty_map, const_def, ty_def} =>
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    67
      {const_map = const_map, ty_map = ty_map,
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    68
       const_def = (Symtab.update (s, th) const_def), ty_def = ty_def}) thy'
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    69
  end
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    70
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    71
fun add_typ_def tyname absname repname th thy =
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    72
  let
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    73
    val th = Thm.legacy_freezeT th
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    74
    val (l, _) = dest_comb (HOLogic.dest_Trueprop (prop_of th))
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    75
    val (l, abst) = dest_comb l
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    76
    val (_, rept) = dest_comb l
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    77
    val (absn, _) = dest_Const abst
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    78
    val (repn, _) = dest_Const rept
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    79
    val nty = domain_type (fastype_of rept)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    80
    val ntyn = fst (dest_Type nty)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    81
    val thy2 = add_typ_map tyname ntyn thy
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    82
    val thy3 = add_const_map absname absn thy2
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    83
    val thy4 = add_const_map repname repn thy3
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    84
  in
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    85
    Data.map (fn {const_map, ty_map, const_def, ty_def} =>
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    86
      {const_map = const_map, ty_map = ty_map,
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    87
       const_def = const_def, ty_def = (Symtab.update (tyname, th) ty_def)}) thy4
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    88
  end
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    89
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    90
val parser = Parse.name -- Scan.option (Parse.$$$ ":" |-- Parse.xname)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    91
fun add_const_attr (s1, s2) = Thm.declaration_attribute
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    92
  (fn th => Context.mapping (add_const_def s1 th s2) (fn x => x))
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    93
val _ = Context.>> (Context.map_theory
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    94
  (Attrib.setup (Binding.name "import_const") (Scan.lift parser >> add_const_attr)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    95
  "Declare a theorem as an equality that maps the given constant"))
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    96
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    97
val parser = Parse.name -- (Parse.name -- Parse.name)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    98
fun add_typ_attr (tyname, (absname, repname)) = Thm.declaration_attribute
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
    99
  (fn th => Context.mapping (add_typ_def tyname absname repname th) (fn x => x))
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   100
val _ = Context.>> (Context.map_theory
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   101
  (Attrib.setup (Binding.name "import_type") (Scan.lift parser >> add_typ_attr)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   102
  "Declare a type_definion theorem as a map for an imported type abs rep"))
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   103
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   104
val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   105
  (fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   106
val _ = Outer_Syntax.command @{command_spec "import_type_map"}
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   107
  "Map external type name to existing Isabelle/HOL type name"
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   108
  (type_map >> Toplevel.theory)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   109
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   110
val const_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   111
  (fn (cname1, cname2) => add_const_map cname1 cname2)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   112
val _ = Outer_Syntax.command @{command_spec "import_const_map"}
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   113
  "Map external const name to existing Isabelle/HOL const name"
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   114
  (const_map >> Toplevel.theory)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   115
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   116
(* Initial type and constant maps, for types and constants that are not
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   117
   defined, which means their definitions do not appear in the proof dump *)
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   118
val _ = Context.>> (Context.map_theory (
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   119
  add_typ_map "bool" @{type_name bool} o
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   120
  add_typ_map "fun" @{type_name fun} o
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   121
  add_typ_map "ind" @{type_name ind} o
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   122
  add_const_map "=" @{const_name HOL.eq} o
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   123
  add_const_map "@" @{const_name "Eps"}))
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   124
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff changeset
   125
end