src/HOL/Import/HOL/prim_rec.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 19277 f7602e74d948
permissions -rw-r--r--
adaptions to codegen_package
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
def_maps
skalberg@14516
     6
  "wellfounded" > "wellfounded_primdef"
skalberg@14516
     7
  "measure" > "measure_primdef"
skalberg@14516
     8
  "SIMP_REC_REL" > "SIMP_REC_REL_def"
skalberg@14516
     9
  "SIMP_REC" > "SIMP_REC_def"
skalberg@14516
    10
  "PRIM_REC_FUN" > "PRIM_REC_FUN_def"
skalberg@14516
    11
  "PRIM_REC" > "PRIM_REC_def"
skalberg@14516
    12
  "PRE" > "PRE_def"
skalberg@14516
    13
skalberg@14516
    14
const_maps
skalberg@14516
    15
  "wellfounded" > "HOL4Base.prim_rec.wellfounded"
skalberg@14516
    16
  "measure" > "HOL4Base.prim_rec.measure"
skalberg@14516
    17
  "SIMP_REC_REL" > "HOL4Base.prim_rec.SIMP_REC_REL"
skalberg@14516
    18
  "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
skalberg@14516
    19
  "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
skalberg@14516
    20
  "PRE" > "HOL4Base.prim_rec.PRE"
skalberg@14516
    21
  "<" > "op <" :: "nat => nat => bool"
skalberg@14516
    22
skalberg@14516
    23
thm_maps
skalberg@14516
    24
  "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
skalberg@14516
    25
  "wellfounded_def" > "HOL4Base.prim_rec.wellfounded_def"
skalberg@14516
    26
  "num_Axiom_old" > "HOL4Base.prim_rec.num_Axiom_old"
skalberg@14516
    27
  "num_Axiom" > "HOL4Base.prim_rec.num_Axiom"
skalberg@14516
    28
  "measure_thm" > "HOL4Base.prim_rec.measure_thm"
skalberg@14516
    29
  "measure_primdef" > "HOL4Base.prim_rec.measure_primdef"
skalberg@14516
    30
  "measure_def" > "HOL4Base.prim_rec.measure_def"
skalberg@14516
    31
  "WF_measure" > "HOL4Base.prim_rec.WF_measure"
skalberg@14516
    32
  "WF_PRED" > "HOL4Base.prim_rec.WF_PRED"
skalberg@14516
    33
  "WF_LESS" > "HOL4Base.prim_rec.WF_LESS"
skalberg@14516
    34
  "WF_IFF_WELLFOUNDED" > "HOL4Base.prim_rec.WF_IFF_WELLFOUNDED"
skalberg@14516
    35
  "SUC_LESS" > "Nat.Suc_lessD"
skalberg@14516
    36
  "SUC_ID" > "Nat.Suc_n_not_n"
skalberg@14516
    37
  "SIMP_REC_THM" > "HOL4Base.prim_rec.SIMP_REC_THM"
skalberg@14516
    38
  "SIMP_REC_REL_def" > "HOL4Base.prim_rec.SIMP_REC_REL_def"
skalberg@14516
    39
  "SIMP_REC_REL_UNIQUE_RESULT" > "HOL4Base.prim_rec.SIMP_REC_REL_UNIQUE_RESULT"
skalberg@14516
    40
  "SIMP_REC_REL_UNIQUE" > "HOL4Base.prim_rec.SIMP_REC_REL_UNIQUE"
skalberg@14516
    41
  "SIMP_REC_REL" > "HOL4Base.prim_rec.SIMP_REC_REL"
skalberg@14516
    42
  "SIMP_REC_EXISTS" > "HOL4Base.prim_rec.SIMP_REC_EXISTS"
skalberg@14516
    43
  "SIMP_REC" > "HOL4Base.prim_rec.SIMP_REC"
skalberg@14516
    44
  "PRIM_REC_def" > "HOL4Base.prim_rec.PRIM_REC_def"
skalberg@14516
    45
  "PRIM_REC_THM" > "HOL4Base.prim_rec.PRIM_REC_THM"
skalberg@14516
    46
  "PRIM_REC_FUN_def" > "HOL4Base.prim_rec.PRIM_REC_FUN_def"
skalberg@14516
    47
  "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
skalberg@14516
    48
  "PRIM_REC_EQN" > "HOL4Base.prim_rec.PRIM_REC_EQN"
skalberg@14516
    49
  "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
skalberg@14516
    50
  "PRE_def" > "HOL4Base.prim_rec.PRE_def"
skalberg@14516
    51
  "PRE_DEF" > "HOL4Base.prim_rec.PRE_DEF"
skalberg@14516
    52
  "PRE" > "HOL4Base.prim_rec.PRE"
skalberg@14516
    53
  "NOT_LESS_EQ" > "HOL4Base.prim_rec.NOT_LESS_EQ"
skalberg@14516
    54
  "NOT_LESS_0" > "Nat.not_less0"
skalberg@14516
    55
  "LESS_THM" > "HOL4Base.prim_rec.LESS_THM"
skalberg@14516
    56
  "LESS_SUC_SUC" > "HOL4Base.prim_rec.LESS_SUC_SUC"
skalberg@14516
    57
  "LESS_SUC_REFL" > "Nat.lessI"
skalberg@14516
    58
  "LESS_SUC_IMP" > "HOL4Base.prim_rec.LESS_SUC_IMP"
skalberg@14516
    59
  "LESS_SUC" > "Nat.less_SucI"
skalberg@14516
    60
  "LESS_REFL" > "Nat.less_not_refl"
skalberg@14516
    61
  "LESS_NOT_EQ" > "Nat.less_not_refl3"
skalberg@14516
    62
  "LESS_MONO" > "Nat.Suc_mono"
skalberg@14516
    63
  "LESS_LEMMA2" > "HOL4Base.prim_rec.LESS_LEMMA2"
skalberg@14516
    64
  "LESS_LEMMA1" > "HOL4Base.prim_rec.LESS_LEMMA1"
skalberg@14516
    65
  "LESS_DEF" > "HOL4Compat.LESS_DEF"
skalberg@14516
    66
  "LESS_0_0" > "HOL4Base.prim_rec.LESS_0_0"
skalberg@14516
    67
  "LESS_0" > "Nat.zero_less_Suc"
skalberg@14516
    68
  "INV_SUC_EQ" > "Nat.nat.simps_3"
skalberg@14516
    69
  "EQ_LESS" > "HOL4Base.prim_rec.EQ_LESS"
skalberg@14516
    70
  "DC" > "HOL4Base.prim_rec.DC"
skalberg@14516
    71
skalberg@14516
    72
end