src/HOL/Import/HOL/bool.imp

   "T" > "True"
   "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
   "RES_FORALL" > "HOL4Base.bool.RES_FORALL"
   "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
   "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS"
-  "ONTO" > "HOL4Setup.ONTO"
+  "ONTO" > "Fun.surj"
   "ONE_ONE" > "HOL4Setup.ONE_ONE"
   "LET" > "HOL4Compat.LET"
   "IN" > "HOL4Base.bool.IN"
   "F" > "False"
   "COND" > "HOL.If"

 
 thm_maps
   "bool_case_thm" > "HOL4Base.bool.bool_case_thm"
   "bool_case_ID" > "HOL4Base.bool.bool_case_ID"
   "bool_case_DEF" > "HOL4Compat.bool_case_DEF"
-  "bool_INDUCT" > "Datatype.bool.induct_correctness"
+  "bool_INDUCT" > "Datatype.bool.induct"
   "boolAxiom" > "HOL4Base.bool.boolAxiom"
   "UNWIND_THM2" > "HOL.simp_thms_39"
   "UNWIND_THM1" > "HOL.simp_thms_40"
-  "UNWIND_FORALL_THM2" > "HOL.simp_thms_41"
+  "UNWIND_FORALL_THM2" > "HOL4Base.bool.UNWIND_FORALL_THM2"
   "UNWIND_FORALL_THM1" > "HOL.simp_thms_42"
   "UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP"
   "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM"
   "T_DEF" > "HOL.True_def"
   "TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION"

   "OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM"
   "OR_ELIM_THM" > "Recdef.tfl_disjE"
   "OR_DEF" > "HOL.or_def"
   "OR_CONG" > "HOL4Base.bool.OR_CONG"
   "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
-  "ONTO_THM" > "HOL4Setup.ONTO_DEF"
-  "ONTO_DEF" > "HOL4Setup.ONTO_DEF"
+  "ONTO_THM" > "Fun.surj_def"
+  "ONTO_DEF" > "Fun.surj_def"
   "ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM"
   "ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF"
   "NOT_IMP" > "HOL.not_imp"
   "NOT_FORALL_THM" > "Inductive.basic_monos_15"
   "NOT_F" > "HOL.Eq_FalseI"

   "NOT_DEF" > "HOL.simp_thms_19"
   "NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES"
   "NOT_AND" > "HOL4Base.bool.NOT_AND"
   "MONO_OR" > "Inductive.basic_monos_3"
   "MONO_NOT" > "HOL.rev_contrapos"
-  "MONO_IMP" > "Set.imp_mono"
+  "MONO_IMP" > "HOL4Base.bool.MONO_IMP"
   "MONO_EXISTS" > "Inductive.basic_monos_5"
   "MONO_COND" > "HOL4Base.bool.MONO_COND"
   "MONO_AND" > "Inductive.basic_monos_4"
   "MONO_ALL" > "Inductive.basic_monos_6"
   "LET_THM" > "HOL.Let_def"

   "LET_DEF" > "HOL4Compat.LET_def"
   "LET_CONG" > "Recdef.let_cong"
   "LEFT_OR_OVER_AND" > "HOL.disj_conj_distribL"
   "LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
   "LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
-  "LEFT_FORALL_IMP_THM" > "HOL.imp_ex"
+  "LEFT_FORALL_IMP_THM" > "HOL4Base.bool.LEFT_FORALL_IMP_THM"
   "LEFT_EXISTS_IMP_THM" > "HOL.imp_all"
   "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
   "LEFT_AND_OVER_OR" > "HOL.conj_disj_distribL"
-  "LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
+  "LEFT_AND_FORALL_THM" > "HOL4Base.bool.LEFT_AND_FORALL_THM"
   "IN_def" > "HOL4Base.bool.IN_def"
   "IN_DEF" > "HOL4Base.bool.IN_DEF"
   "INFINITY_AX" > "HOL4Setup.INFINITY_AX"
   "IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F"
   "IMP_F" > "HOL.notI"

   "EQ_TRANS" > "Set.basic_trans_rules_31"
   "EQ_SYM_EQ" > "HOL.eq_sym_conv"
   "EQ_SYM" > "HOL.meta_eq_to_obj_eq"
   "EQ_REFL" > "Presburger.fm_modd_pinf"
   "EQ_IMP_THM" > "HOL.iff_conv_conj_imp"
-  "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
+  "EQ_EXT" > "HOL4Base.bool.EQ_EXT"
   "EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND"
   "EQ_CLAUSES" > "HOL4Base.bool.EQ_CLAUSES"
   "DISJ_SYM" > "HOL.disj_comms_1"
   "DISJ_IMP_THM" > "HOL.imp_disjL"
   "DISJ_COMM" > "HOL.disj_comms_1"