--- a/src/HOL/Import/hol4rews.ML Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Sat Oct 17 14:43:18 2009 +0200
@@ -7,7 +7,7 @@
type holthm = (term * term) list * thm
datatype ImportStatus =
- NoImport
+ NoImport
| Generating of string
| Replaying of string
@@ -81,10 +81,10 @@
fun set_segment thyname segname thy =
let
- val imps = HOL4Imports.get thy
- val imps' = Symtab.update_new (thyname,segname) imps
+ val imps = HOL4Imports.get thy
+ val imps' = Symtab.update_new (thyname,segname) imps
in
- HOL4Imports.put imps' thy
+ HOL4Imports.put imps' thy
end
structure HOL4CMoves = TheoryDataFun
@@ -176,42 +176,42 @@
in
fun add_hol4_rewrite (Context.Theory thy, th) =
let
- val _ = message "Adding HOL4 rewrite"
- val th1 = th RS eq_reflection
- val current_rews = HOL4Rewrites.get thy
- val new_rews = insert Thm.eq_thm th1 current_rews
- val updated_thy = HOL4Rewrites.put new_rews thy
+ val _ = message "Adding HOL4 rewrite"
+ val th1 = th RS eq_reflection
+ val current_rews = HOL4Rewrites.get thy
+ val new_rews = insert Thm.eq_thm th1 current_rews
+ val updated_thy = HOL4Rewrites.put new_rews thy
in
- (Context.Theory updated_thy,th1)
+ (Context.Theory updated_thy,th1)
end
| add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
end
fun ignore_hol4 bthy bthm thy =
let
- val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
- val curmaps = HOL4Maps.get thy
- val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
- val upd_thy = HOL4Maps.put newmaps thy
+ val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
+ val curmaps = HOL4Maps.get thy
+ val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
+ val upd_thy = HOL4Maps.put newmaps thy
in
- upd_thy
+ upd_thy
end
val opt_get_output_thy = #2 o HOL4Dump.get
fun get_output_thy thy =
case #2 (HOL4Dump.get thy) of
- "" => error "No theory file being output"
+ "" => error "No theory file being output"
| thyname => thyname
val get_output_dir = #1 o HOL4Dump.get
fun add_hol4_move bef aft thy =
let
- val curmoves = HOL4Moves.get thy
- val newmoves = Symtab.update_new (bef, aft) curmoves
+ val curmoves = HOL4Moves.get thy
+ val newmoves = Symtab.update_new (bef, aft) curmoves
in
- HOL4Moves.put newmoves thy
+ HOL4Moves.put newmoves thy
end
fun get_hol4_move bef thy =
@@ -219,21 +219,21 @@
fun follow_name thmname thy =
let
- val moves = HOL4Moves.get thy
- fun F thmname =
- case Symtab.lookup moves thmname of
- SOME name => F name
- | NONE => thmname
+ val moves = HOL4Moves.get thy
+ fun F thmname =
+ case Symtab.lookup moves thmname of
+ SOME name => F name
+ | NONE => thmname
in
- F thmname
+ F thmname
end
fun add_hol4_cmove bef aft thy =
let
- val curmoves = HOL4CMoves.get thy
- val newmoves = Symtab.update_new (bef, aft) curmoves
+ val curmoves = HOL4CMoves.get thy
+ val newmoves = Symtab.update_new (bef, aft) curmoves
in
- HOL4CMoves.put newmoves thy
+ HOL4CMoves.put newmoves thy
end
fun get_hol4_cmove bef thy =
@@ -241,128 +241,128 @@
fun follow_cname thmname thy =
let
- val moves = HOL4CMoves.get thy
- fun F thmname =
- case Symtab.lookup moves thmname of
- SOME name => F name
- | NONE => thmname
+ val moves = HOL4CMoves.get thy
+ fun F thmname =
+ case Symtab.lookup moves thmname of
+ SOME name => F name
+ | NONE => thmname
in
- F thmname
+ F thmname
end
fun add_hol4_mapping bthy bthm isathm thy =
- let
+ let
(* val _ = writeln ("Before follow_name: "^isathm) *)
val isathm = follow_name isathm thy
(* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
- val curmaps = HOL4Maps.get thy
- val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
- val upd_thy = HOL4Maps.put newmaps thy
+ val curmaps = HOL4Maps.get thy
+ val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
+ val upd_thy = HOL4Maps.put newmaps thy
in
- upd_thy
+ upd_thy
end;
fun get_hol4_type_mapping bthy tycon thy =
let
- val maps = HOL4TypeMaps.get thy
+ val maps = HOL4TypeMaps.get thy
in
- StringPair.lookup maps (bthy,tycon)
+ StringPair.lookup maps (bthy,tycon)
end
fun get_hol4_mapping bthy bthm thy =
let
- val curmaps = HOL4Maps.get thy
+ val curmaps = HOL4Maps.get thy
in
- StringPair.lookup curmaps (bthy,bthm)
+ StringPair.lookup curmaps (bthy,bthm)
end;
fun add_hol4_const_mapping bthy bconst internal isaconst thy =
let
- val thy = case opt_get_output_thy thy of
- "" => thy
- | output_thy => if internal
- then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
- else thy
- val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
- val curmaps = HOL4ConstMaps.get thy
- val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
- val upd_thy = HOL4ConstMaps.put newmaps thy
+ val thy = case opt_get_output_thy thy of
+ "" => thy
+ | output_thy => if internal
+ then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+ else thy
+ val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
+ val curmaps = HOL4ConstMaps.get thy
+ val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
+ val upd_thy = HOL4ConstMaps.put newmaps thy
in
- upd_thy
+ upd_thy
end;
fun add_hol4_const_renaming bthy bconst newname thy =
let
- val currens = HOL4Rename.get thy
- val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
- val newrens = StringPair.update_new ((bthy,bconst),newname) currens
- val upd_thy = HOL4Rename.put newrens thy
+ val currens = HOL4Rename.get thy
+ val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
+ val newrens = StringPair.update_new ((bthy,bconst),newname) currens
+ val upd_thy = HOL4Rename.put newrens thy
in
- upd_thy
+ upd_thy
end;
fun get_hol4_const_renaming bthy bconst thy =
let
- val currens = HOL4Rename.get thy
+ val currens = HOL4Rename.get thy
in
- StringPair.lookup currens (bthy,bconst)
+ StringPair.lookup currens (bthy,bconst)
end;
fun get_hol4_const_mapping bthy bconst thy =
let
- val bconst = case get_hol4_const_renaming bthy bconst thy of
- SOME name => name
- | NONE => bconst
- val maps = HOL4ConstMaps.get thy
+ val bconst = case get_hol4_const_renaming bthy bconst thy of
+ SOME name => name
+ | NONE => bconst
+ val maps = HOL4ConstMaps.get thy
in
- StringPair.lookup maps (bthy,bconst)
+ StringPair.lookup maps (bthy,bconst)
end
fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
let
- val thy = case opt_get_output_thy thy of
- "" => thy
- | output_thy => if internal
- then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
- else thy
- val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
- val curmaps = HOL4ConstMaps.get thy
- val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
- val upd_thy = HOL4ConstMaps.put newmaps thy
+ val thy = case opt_get_output_thy thy of
+ "" => thy
+ | output_thy => if internal
+ then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
+ else thy
+ val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
+ val curmaps = HOL4ConstMaps.get thy
+ val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
+ val upd_thy = HOL4ConstMaps.put newmaps thy
in
- upd_thy
+ upd_thy
end;
fun add_hol4_type_mapping bthy bconst internal isaconst thy =
let
- val curmaps = HOL4TypeMaps.get thy
- val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
- val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
+ val curmaps = HOL4TypeMaps.get thy
+ val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
+ val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
val upd_thy = HOL4TypeMaps.put newmaps thy
in
- upd_thy
+ upd_thy
end;
fun add_hol4_pending bthy bthm hth thy =
let
- val thmname = Sign.full_bname thy bthm
- val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
- val curpend = HOL4Pending.get thy
- val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
- val upd_thy = HOL4Pending.put newpend thy
- val thy' = case opt_get_output_thy upd_thy of
- "" => add_hol4_mapping bthy bthm thmname upd_thy
- | output_thy =>
- let
- val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
- in
- upd_thy |> add_hol4_move thmname new_thmname
- |> add_hol4_mapping bthy bthm new_thmname
- end
+ val thmname = Sign.full_bname thy bthm
+ val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
+ val curpend = HOL4Pending.get thy
+ val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
+ val upd_thy = HOL4Pending.put newpend thy
+ val thy' = case opt_get_output_thy upd_thy of
+ "" => add_hol4_mapping bthy bthm thmname upd_thy
+ | output_thy =>
+ let
+ val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
+ in
+ upd_thy |> add_hol4_move thmname new_thmname
+ |> add_hol4_mapping bthy bthm new_thmname
+ end
in
- thy'
+ thy'
end;
fun get_hol4_theorem thyname thmname thy =
@@ -404,79 +404,79 @@
fun add_dump str thy =
let
- val (dir,thyname,curdump) = HOL4Dump.get thy
+ val (dir,thyname,curdump) = HOL4Dump.get thy
in
- HOL4Dump.put (dir,thyname,str::curdump) thy
+ HOL4Dump.put (dir,thyname,str::curdump) thy
end
fun flush_dump thy =
let
- val (dir,thyname,dumpdata) = HOL4Dump.get thy
- val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
- file=thyname ^ ".thy"})
- val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
- val _ = TextIO.closeOut os
+ val (dir,thyname,dumpdata) = HOL4Dump.get thy
+ val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
+ file=thyname ^ ".thy"})
+ val _ = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
+ val _ = TextIO.closeOut os
in
- HOL4Dump.put ("","",[]) thy
+ HOL4Dump.put ("","",[]) thy
end
fun set_generating_thy thyname thy =
case HOL4DefThy.get thy of
- NoImport => HOL4DefThy.put (Generating thyname) thy
+ NoImport => HOL4DefThy.put (Generating thyname) thy
| _ => error "Import already in progess"
fun set_replaying_thy thyname thy =
case HOL4DefThy.get thy of
- NoImport => HOL4DefThy.put (Replaying thyname) thy
+ NoImport => HOL4DefThy.put (Replaying thyname) thy
| _ => error "Import already in progess"
fun clear_import_thy thy =
case HOL4DefThy.get thy of
- NoImport => error "No import in progress"
+ NoImport => error "No import in progress"
| _ => HOL4DefThy.put NoImport thy
fun get_generating_thy thy =
case HOL4DefThy.get thy of
- Generating thyname => thyname
+ Generating thyname => thyname
| _ => error "No theory being generated"
fun get_replaying_thy thy =
case HOL4DefThy.get thy of
- Replaying thyname => thyname
+ Replaying thyname => thyname
| _ => error "No theory being replayed"
fun get_import_thy thy =
case HOL4DefThy.get thy of
- Replaying thyname => thyname
+ Replaying thyname => thyname
| Generating thyname => thyname
| _ => error "No theory being imported"
fun should_ignore thyname thy thmname =
case get_hol4_mapping thyname thmname thy of
- SOME NONE => true
+ SOME NONE => true
| _ => false
val trans_string =
let
- fun quote s = "\"" ^ s ^ "\""
- fun F [] = []
- | F (#"\\" :: cs) = patch #"\\" cs
- | F (#"\"" :: cs) = patch #"\"" cs
- | F (c :: cs) = c :: F cs
- and patch c rest = #"\\" :: c :: F rest
+ fun quote s = "\"" ^ s ^ "\""
+ fun F [] = []
+ | F (#"\\" :: cs) = patch #"\\" cs
+ | F (#"\"" :: cs) = patch #"\"" cs
+ | F (c :: cs) = c :: F cs
+ and patch c rest = #"\\" :: c :: F rest
in
- quote o String.implode o F o String.explode
+ quote o String.implode o F o String.explode
end
fun dump_import_thy thyname thy =
let
- val output_dir = get_output_dir thy
- val output_thy = get_output_thy thy
- val input_thy = Context.theory_name thy
- val import_segment = get_import_segment thy
- val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
- file=thyname ^ ".imp"})
- fun out s = TextIO.output(os,s)
+ val output_dir = get_output_dir thy
+ val output_thy = get_output_thy thy
+ val input_thy = Context.theory_name thy
+ val import_segment = get_import_segment thy
+ val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
+ file=thyname ^ ".imp"})
+ fun out s = TextIO.output(os,s)
val (ignored, mapped) = StringPair.fold
(fn ((bthy, bthm), v) => fn (ign, map) =>
if bthy = thyname
@@ -490,141 +490,141 @@
val constrenames = mk (HOL4Rename.get thy);
val typemaps = mk (HOL4TypeMaps.get thy);
val defmaps = mk (HOL4DefMaps.get thy);
- fun new_name internal isa =
- if internal
- then
- let
- val paths = Long_Name.explode isa
- val i = Library.drop(length paths - 2,paths)
- in
- case i of
- [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
- | _ => error "hol4rews.dump internal error"
- end
- else
- isa
+ fun new_name internal isa =
+ if internal
+ then
+ let
+ val paths = Long_Name.explode isa
+ val i = Library.drop(length paths - 2,paths)
+ in
+ case i of
+ [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
+ | _ => error "hol4rews.dump internal error"
+ end
+ else
+ isa
- val _ = out "import\n\n"
+ val _ = out "import\n\n"
- val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
- val _ = if null defmaps
- then ()
- else out "def_maps"
- val _ = app (fn (hol,isa) =>
- out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
- val _ = if null defmaps
- then ()
- else out "\n\n"
+ val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
+ val _ = if null defmaps
+ then ()
+ else out "def_maps"
+ val _ = app (fn (hol,isa) =>
+ out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
+ val _ = if null defmaps
+ then ()
+ else out "\n\n"
- val _ = if null typemaps
- then ()
- else out "type_maps"
- val _ = app (fn (hol,(internal,isa)) =>
- out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
- val _ = if null typemaps
- then ()
- else out "\n\n"
+ val _ = if null typemaps
+ then ()
+ else out "type_maps"
+ val _ = app (fn (hol,(internal,isa)) =>
+ out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
+ val _ = if null typemaps
+ then ()
+ else out "\n\n"
- val _ = if null constmaps
- then ()
- else out "const_maps"
- val _ = app (fn (hol,(internal,isa,opt_ty)) =>
- (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
- case opt_ty of
- SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
- | NONE => ())) constmaps
- val _ = if null constmaps
- then ()
- else out "\n\n"
+ val _ = if null constmaps
+ then ()
+ else out "const_maps"
+ val _ = app (fn (hol,(internal,isa,opt_ty)) =>
+ (out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
+ case opt_ty of
+ SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
+ | NONE => ())) constmaps
+ val _ = if null constmaps
+ then ()
+ else out "\n\n"
- val _ = if null constrenames
- then ()
- else out "const_renames"
- val _ = app (fn (old,new) =>
- out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
- val _ = if null constrenames
- then ()
- else out "\n\n"
+ val _ = if null constrenames
+ then ()
+ else out "const_renames"
+ val _ = app (fn (old,new) =>
+ out ("\n " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
+ val _ = if null constrenames
+ then ()
+ else out "\n\n"
- fun gen2replay in_thy out_thy s =
- let
- val ss = Long_Name.explode s
- in
- if (hd ss = in_thy) then
- Long_Name.implode (out_thy::(tl ss))
- else
- s
- end
+ fun gen2replay in_thy out_thy s =
+ let
+ val ss = Long_Name.explode s
+ in
+ if (hd ss = in_thy) then
+ Long_Name.implode (out_thy::(tl ss))
+ else
+ s
+ end
- val _ = if null mapped
- then ()
- else out "thm_maps"
- val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
- val _ = if null mapped
- then ()
- else out "\n\n"
+ val _ = if null mapped
+ then ()
+ else out "thm_maps"
+ val _ = app (fn (hol,isa) => out ("\n " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
+ val _ = if null mapped
+ then ()
+ else out "\n\n"
- val _ = if null ignored
- then ()
- else out "ignore_thms"
- val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored
- val _ = if null ignored
- then ()
- else out "\n\n"
+ val _ = if null ignored
+ then ()
+ else out "ignore_thms"
+ val _ = app (fn ign => out ("\n " ^ (trans_string ign))) ignored
+ val _ = if null ignored
+ then ()
+ else out "\n\n"
- val _ = out "end\n"
- val _ = TextIO.closeOut os
+ val _ = out "end\n"
+ val _ = TextIO.closeOut os
in
- thy
+ thy
end
fun set_used_names names thy =
let
- val unames = HOL4UNames.get thy
+ val unames = HOL4UNames.get thy
in
- case unames of
- [] => HOL4UNames.put names thy
- | _ => error "hol4rews.set_used_names called on initialized data!"
+ case unames of
+ [] => HOL4UNames.put names thy
+ | _ => error "hol4rews.set_used_names called on initialized data!"
end
val clear_used_names = HOL4UNames.put [];
fun get_defmap thyname const thy =
let
- val maps = HOL4DefMaps.get thy
+ val maps = HOL4DefMaps.get thy
in
- StringPair.lookup maps (thyname,const)
+ StringPair.lookup maps (thyname,const)
end
fun add_defmap thyname const defname thy =
let
- val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
- val maps = HOL4DefMaps.get thy
- val maps' = StringPair.update_new ((thyname,const),defname) maps
- val thy' = HOL4DefMaps.put maps' thy
+ val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
+ val maps = HOL4DefMaps.get thy
+ val maps' = StringPair.update_new ((thyname,const),defname) maps
+ val thy' = HOL4DefMaps.put maps' thy
in
- thy'
+ thy'
end
fun get_defname thyname name thy =
let
- val maps = HOL4DefMaps.get thy
- fun F dname = (dname,add_defmap thyname name dname thy)
+ val maps = HOL4DefMaps.get thy
+ fun F dname = (dname,add_defmap thyname name dname thy)
in
- case StringPair.lookup maps (thyname,name) of
- SOME thmname => (thmname,thy)
- | NONE =>
- let
- val used = HOL4UNames.get thy
- val defname = Thm.def_name name
- val pdefname = name ^ "_primdef"
- in
- if not (defname mem used)
- then F defname (* name_def *)
- else if not (pdefname mem used)
- then F pdefname (* name_primdef *)
- else F (Name.variant used pdefname) (* last resort *)
- end
+ case StringPair.lookup maps (thyname,name) of
+ SOME thmname => (thmname,thy)
+ | NONE =>
+ let
+ val used = HOL4UNames.get thy
+ val defname = Thm.def_name name
+ val pdefname = name ^ "_primdef"
+ in
+ if not (defname mem used)
+ then F defname (* name_def *)
+ else if not (pdefname mem used)
+ then F pdefname (* name_primdef *)
+ else F (Name.variant used pdefname) (* last resort *)
+ end
end
local
@@ -639,12 +639,12 @@
local
fun initial_maps thy =
- thy |> add_hol4_type_mapping "min" "bool" false "bool"
- |> add_hol4_type_mapping "min" "fun" false "fun"
- |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
- |> add_hol4_const_mapping "min" "=" false "op ="
- |> add_hol4_const_mapping "min" "==>" false "op -->"
- |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
+ thy |> add_hol4_type_mapping "min" "bool" false "bool"
+ |> add_hol4_type_mapping "min" "fun" false "fun"
+ |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
+ |> add_hol4_const_mapping "min" "=" false "op ="
+ |> add_hol4_const_mapping "min" "==>" false "op -->"
+ |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
in
val hol4_setup =
initial_maps #>