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