src/HOL/Hyperreal/transfer.ML
changeset 17429 e8d6ed3aacfe
parent 17333 605c97701833
child 17432 835647238122
     1.1 --- a/src/HOL/Hyperreal/transfer.ML	Thu Sep 15 23:16:04 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/transfer.ML	Thu Sep 15 23:46:22 2005 +0200
     1.3 @@ -8,17 +8,13 @@
     1.4  signature TRANSFER_TAC =
     1.5  sig
     1.6    val transfer_tac: thm list -> int -> tactic
     1.7 +  val add_const: string -> theory -> theory
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11  structure Transfer: TRANSFER_TAC =
    1.12  struct
    1.13  
    1.14 -(* TODO: make this list extensible *)
    1.15 -val star_consts =
    1.16 -  [ "StarType.star_of", "StarType.Ifun"
    1.17 -  , "StarType.unstar", "StarType.Iset" ]
    1.18 -
    1.19  structure TransferData = TheoryDataFun
    1.20  (struct
    1.21    val name = "HOL/transfer";
    1.22 @@ -28,7 +24,7 @@
    1.23      refolds: thm list,
    1.24      consts: string list
    1.25    };
    1.26 -  val empty = {intros = [], unfolds = [], refolds = [], consts = star_consts};
    1.27 +  val empty = {intros = [], unfolds = [], refolds = [], consts = []};
    1.28    val copy = I;
    1.29    val extend = I;
    1.30    fun merge _
    1.31 @@ -45,7 +41,7 @@
    1.32  
    1.33  val transfer_start = thm "transfer_start"
    1.34  
    1.35 -fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
    1.36 +fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
    1.37    | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
    1.38    | unstar_typ T = T
    1.39  
    1.40 @@ -102,10 +98,6 @@
    1.41  fun map_refolds f = TransferData.map
    1.42    (fn {intros,unfolds,refolds,consts} =>
    1.43      {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
    1.44 -
    1.45 -fun map_consts f = TransferData.map
    1.46 -  (fn {intros,unfolds,refolds,consts} =>
    1.47 -    {intros=intros, unfolds=unfolds, refolds=refolds, consts=f consts})
    1.48  in
    1.49  fun intro_add_global (thy, thm) = (map_intros (Drule.add_rule thm) thy, thm);
    1.50  fun intro_del_global (thy, thm) = (map_intros (Drule.del_rule thm) thy, thm);
    1.51 @@ -117,6 +109,10 @@
    1.52  fun refold_del_global (thy, thm) = (map_refolds (Drule.del_rule thm) thy, thm);
    1.53  end
    1.54  
    1.55 +fun add_const c = TransferData.map
    1.56 +  (fn {intros,unfolds,refolds,consts} =>
    1.57 +    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})
    1.58 +
    1.59  local
    1.60    val undef_local =
    1.61      Attrib.add_del_args