--- a/src/HOL/Import/HOL/bool.imp Mon Sep 26 02:06:44 2005 +0200
+++ b/src/HOL/Import/HOL/bool.imp Mon Sep 26 02:27:14 2005 +0200
@@ -21,7 +21,7 @@
"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"
@@ -37,11 +37,11 @@
"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"
@@ -82,8 +82,8 @@
"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"
@@ -95,7 +95,7 @@
"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"
@@ -108,11 +108,11 @@
"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"
@@ -146,7 +146,7 @@
"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"