src/HOL/Import/HOL/bool.imp

   "RES_EXISTS" > "RES_EXISTS_def"
   "RES_ABSTRACT" > "RES_ABSTRACT_def"
   "IN" > "IN_def"
   "ARB" > "ARB_def"
 
+type_maps
+  "bool" > "HOL.bool"
+
 const_maps
   "~" > "HOL.Not"
-  "bool_case" > "Datatype.bool.bool_case"
-  "\\/" > HOL.disj
+  "bool_case" > "Product_Type.bool.bool_case"
+  "\\/" > "HOL.disj"
   "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
   "T" > "HOL.True"
   "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
   "RES_FORALL" > "HOL4Base.bool.RES_FORALL"
   "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"

   "F" > "HOL.False"
   "COND" > "HOL.If"
   "ARB" > "HOL4Base.bool.ARB"
   "?!" > "HOL.Ex1"
   "?" > "HOL.Ex"
-  "/\\" > HOL.conj
+  "/\\" > "HOL.conj"
   "!" > "HOL.All"
 
 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" > "Product_Type.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_THM1" > "HOL.simp_thms_42"

   "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM"
   "T_DEF" > "HOL.True_def"
   "TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION"
   "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
   "TRUTH" > "HOL.TrueI"
-  "SWAP_FORALL_THM" > "HOL4Base.bool.SWAP_FORALL_THM"
-  "SWAP_EXISTS_THM" > "HOL4Base.bool.SWAP_EXISTS_THM"
+  "SWAP_FORALL_THM" > "HOL.all_comm"
+  "SWAP_EXISTS_THM" > "HOL.ex_comm"
   "SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM"
   "SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE"
   "SELECT_THM" > "HOL4Setup.EXISTS_DEF"
   "SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial"
   "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
-  "SELECT_AX" > "Hilbert_Choice.tfl_some"
+  "SELECT_AX" > "Hilbert_Choice.someI"
   "RIGHT_OR_OVER_AND" > "HOL.disj_conj_distribR"
   "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
   "RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
   "RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
   "RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
   "RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
-  "RIGHT_AND_OVER_OR" > "HOL.conj_disj_distribR"
+  "RIGHT_AND_OVER_OR" > "Groebner_Basis.dnf_2"
   "RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
   "RES_SELECT_def" > "HOL4Base.bool.RES_SELECT_def"
   "RES_SELECT_DEF" > "HOL4Base.bool.RES_SELECT_DEF"
   "RES_FORALL_def" > "HOL4Base.bool.RES_FORALL_def"
   "RES_FORALL_DEF" > "HOL4Base.bool.RES_FORALL_DEF"
   "RES_EXISTS_def" > "HOL4Base.bool.RES_EXISTS_def"
   "RES_EXISTS_UNIQUE_def" > "HOL4Base.bool.RES_EXISTS_UNIQUE_def"
   "RES_EXISTS_UNIQUE_DEF" > "HOL4Base.bool.RES_EXISTS_UNIQUE_DEF"
   "RES_EXISTS_DEF" > "HOL4Base.bool.RES_EXISTS_DEF"
   "RES_ABSTRACT_DEF" > "HOL4Base.bool.RES_ABSTRACT_DEF"
-  "REFL_CLAUSE" > "HOL.simp_thms_6"
+  "REFL_CLAUSE" > "Groebner_Basis.bool_simps_6"
   "OR_INTRO_THM2" > "HOL.disjI2"
   "OR_INTRO_THM1" > "HOL.disjI1"
   "OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM"
-  "OR_ELIM_THM" > "Recdef.tfl_disjE"
+  "OR_ELIM_THM" > "HOL.disjE"
   "OR_DEF" > "HOL.or_def"
   "OR_CONG" > "HOL4Base.bool.OR_CONG"
   "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
   "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_EXISTS_THM" > "Inductive.basic_monos_16"
-  "NOT_DEF" > "HOL.simp_thms_19"
+  "NOT_FORALL_THM" > "HOL.not_all"
+  "NOT_F" > "Groebner_Basis.PFalse_2"
+  "NOT_EXISTS_THM" > "HOL.not_ex"
+  "NOT_DEF" > "Groebner_Basis.bool_simps_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_NOT" > "HOL.contrapos_nn"
   "MONO_IMP" > "Set.imp_mono"
   "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_RATOR" > "HOL4Base.bool.LET_RATOR"
   "LET_RAND" > "HOL4Base.bool.LET_RAND"
   "LET_DEF" > "HOL4Compat.LET_def"
-  "LET_CONG" > "Recdef.let_cong"
+  "LET_CONG" > "FunDef.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_EXISTS_IMP_THM" > "HOL.imp_all"
+  "LEFT_FORALL_IMP_THM" > "HOL.all_simps_5"
+  "LEFT_EXISTS_IMP_THM" > "HOL.ex_simps_5"
   "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
-  "LEFT_AND_OVER_OR" > "HOL.conj_disj_distribL"
+  "LEFT_AND_OVER_OR" > "Groebner_Basis.dnf_1"
   "LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
   "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"
-  "IMP_DISJ_THM" > "Inductive.basic_monos_11"
+  "IMP_DISJ_THM" > "Groebner_Basis.nnf_simps_3"
   "IMP_CONG" > "HOL.imp_cong"
   "IMP_CLAUSES" > "HOL4Base.bool.IMP_CLAUSES"
-  "IMP_ANTISYM_AX" > "HOL4Setup.light_imp_as"
+  "IMP_ANTISYM_AX" > "HOL.iff"
   "F_IMP" > "HOL4Base.bool.F_IMP"
   "F_DEF" > "HOL.False_def"
-  "FUN_EQ_THM" > "Fun.fun_eq_iff"
+  "FUN_EQ_THM" > "HOL.fun_eq_iff"
   "FORALL_THM" > "HOL4Base.bool.FORALL_THM"
   "FORALL_SIMP" > "HOL.simp_thms_35"
   "FORALL_DEF" > "HOL.All_def"
   "FORALL_AND_THM" > "HOL.all_conj_distrib"
   "FALSITY" > "HOL.FalseE"

   "EXISTS_SIMP" > "HOL.simp_thms_36"
   "EXISTS_REFL" > "HOL.simp_thms_37"
   "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
   "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
   "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
-  "ETA_THM" > "Presburger.fm_modd_pinf"
-  "ETA_AX" > "Presburger.fm_modd_pinf"
-  "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"
+  "ETA_THM" > "HOL.eta_contract_eq"
+  "ETA_AX" > "HOL.eta_contract_eq"
+  "EQ_TRANS" > "HOL.trans"
+  "EQ_SYM_EQ" > "HOL.eq_ac_1"
+  "EQ_SYM" > "HOL.eq_reflection"
+  "EQ_REFL" > "HOL.refl"
   "EQ_IMP_THM" > "HOL.iff_conv_conj_imp"
-  "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
-  "EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND"
+  "EQ_EXT" > "HOL.eq_reflection"
+  "EQ_EXPAND" > "Groebner_Basis.nnf_simps_4"
   "EQ_CLAUSES" > "HOL4Base.bool.EQ_CLAUSES"
-  "DISJ_SYM" > "HOL.disj_comms_1"
+  "DISJ_SYM" > "Groebner_Basis.dnf_4"
   "DISJ_IMP_THM" > "HOL.imp_disjL"
-  "DISJ_COMM" > "HOL.disj_comms_1"
-  "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
+  "DISJ_COMM" > "Groebner_Basis.dnf_4"
+  "DISJ_ASSOC" > "HOL.disj_ac_3"
   "DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM"
-  "CONJ_SYM" > "HOL.conj_comms_1"
-  "CONJ_COMM" > "HOL.conj_comms_1"
-  "CONJ_ASSOC" > "HOL.conj_assoc"
+  "CONJ_SYM" > "Groebner_Basis.dnf_3"
+  "CONJ_COMM" > "Groebner_Basis.dnf_3"
+  "CONJ_ASSOC" > "HOL.conj_ac_3"
   "COND_RATOR" > "HOL4Base.bool.COND_RATOR"
   "COND_RAND" > "HOL.if_distrib"
   "COND_ID" > "HOL.if_cancel"
   "COND_EXPAND" > "HOL4Base.bool.COND_EXPAND"
   "COND_DEF" > "HOL4Compat.COND_DEF"

   "BOTH_EXISTS_IMP_THM" > "HOL4Base.bool.BOTH_EXISTS_IMP_THM"
   "BOTH_EXISTS_AND_THM" > "HOL4Base.bool.BOTH_EXISTS_AND_THM"
   "BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT"
   "BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM"
   "BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT"
-  "BOOL_CASES_AX" > "Datatype.bool.nchotomy"
-  "BETA_THM" > "Presburger.fm_modd_pinf"
+  "BOOL_CASES_AX" > "HOL.True_or_False"
+  "BETA_THM" > "HOL.eta_contract_eq"
   "ARB_def" > "HOL4Base.bool.ARB_def"
   "ARB_DEF" > "HOL4Base.bool.ARB_DEF"
   "AND_INTRO_THM" > "HOL.conjI"
   "AND_IMP_INTRO" > "HOL.imp_conjL"
   "AND_DEF" > "HOL.and_def"
   "AND_CONG" > "HOL4Base.bool.AND_CONG"
   "AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES"
   "AND2_THM" > "HOL.conjunct2"
   "AND1_THM" > "HOL.conjunct1"
-  "ABS_SIMP" > "Presburger.fm_modd_pinf"
+  "ABS_SIMP" > "HOL.refl"
   "ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM"
 
 ignore_thms
   "UNBOUNDED_THM"
   "UNBOUNDED_DEF"