import
import_segment "hol4"
def_maps
"wellfounded" > "wellfounded_primdef"
"measure" > "measure_primdef"
"SIMP_REC_REL" > "SIMP_REC_REL_def"
"SIMP_REC" > "SIMP_REC_def"
"PRIM_REC_FUN" > "PRIM_REC_FUN_def"
"PRIM_REC" > "PRIM_REC_def"
"PRE" > "PRE_def"
const_maps
"wellfounded" > "HOL4Base.prim_rec.wellfounded"
"measure" > "HOL4Base.prim_rec.measure"
"SIMP_REC_REL" > "HOL4Base.prim_rec.SIMP_REC_REL"
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
"PRE" > "HOL4Base.prim_rec.PRE"
"<" > "Algebras.less" :: "nat => nat => bool"
thm_maps
"wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
"wellfounded_def" > "HOL4Base.prim_rec.wellfounded_def"
"num_Axiom_old" > "HOL4Base.prim_rec.num_Axiom_old"
"num_Axiom" > "HOL4Base.prim_rec.num_Axiom"
"measure_thm" > "HOL4Base.prim_rec.measure_thm"
"measure_primdef" > "HOL4Base.prim_rec.measure_primdef"
"measure_def" > "HOL4Base.prim_rec.measure_def"
"WF_measure" > "HOL4Base.prim_rec.WF_measure"
"WF_PRED" > "HOL4Base.prim_rec.WF_PRED"
"WF_LESS" > "HOL4Base.prim_rec.WF_LESS"
"WF_IFF_WELLFOUNDED" > "HOL4Base.prim_rec.WF_IFF_WELLFOUNDED"
"SUC_LESS" > "Nat.Suc_lessD"
"SUC_ID" > "Nat.Suc_n_not_n"
"SIMP_REC_THM" > "HOL4Base.prim_rec.SIMP_REC_THM"
"SIMP_REC_REL_def" > "HOL4Base.prim_rec.SIMP_REC_REL_def"
"SIMP_REC_REL_UNIQUE_RESULT" > "HOL4Base.prim_rec.SIMP_REC_REL_UNIQUE_RESULT"
"SIMP_REC_REL_UNIQUE" > "HOL4Base.prim_rec.SIMP_REC_REL_UNIQUE"
"SIMP_REC_REL" > "HOL4Base.prim_rec.SIMP_REC_REL"
"SIMP_REC_EXISTS" > "HOL4Base.prim_rec.SIMP_REC_EXISTS"
"SIMP_REC" > "HOL4Base.prim_rec.SIMP_REC"
"PRIM_REC_def" > "HOL4Base.prim_rec.PRIM_REC_def"
"PRIM_REC_THM" > "HOL4Base.prim_rec.PRIM_REC_THM"
"PRIM_REC_FUN_def" > "HOL4Base.prim_rec.PRIM_REC_FUN_def"
"PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
"PRIM_REC_EQN" > "HOL4Base.prim_rec.PRIM_REC_EQN"
"PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
"PRE_def" > "HOL4Base.prim_rec.PRE_def"
"PRE_DEF" > "HOL4Base.prim_rec.PRE_DEF"
"PRE" > "HOL4Base.prim_rec.PRE"
"NOT_LESS_EQ" > "HOL4Base.prim_rec.NOT_LESS_EQ"
"NOT_LESS_0" > "Nat.not_less0"
"LESS_THM" > "HOL4Base.prim_rec.LESS_THM"
"LESS_SUC_SUC" > "HOL4Base.prim_rec.LESS_SUC_SUC"
"LESS_SUC_REFL" > "Nat.lessI"
"LESS_SUC_IMP" > "HOL4Base.prim_rec.LESS_SUC_IMP"
"LESS_SUC" > "Nat.less_SucI"
"LESS_REFL" > "Nat.less_not_refl"
"LESS_NOT_EQ" > "Nat.less_not_refl3"
"LESS_MONO" > "Nat.Suc_mono"
"LESS_LEMMA2" > "HOL4Base.prim_rec.LESS_LEMMA2"
"LESS_LEMMA1" > "HOL4Base.prim_rec.LESS_LEMMA1"
"LESS_DEF" > "HOL4Compat.LESS_DEF"
"LESS_0_0" > "HOL4Base.prim_rec.LESS_0_0"
"LESS_0" > "Nat.zero_less_Suc"
"INV_SUC_EQ" > "Nat.nat.simps_3"
"EQ_LESS" > "HOL4Base.prim_rec.EQ_LESS"
"DC" > "HOL4Base.prim_rec.DC"
end