# HG changeset patch # User wenzelm # Date 1127755155 -7200 # Node ID ab7954ba5261787995cb84cfd496e8a7a2e80b15 # Parent 2f5f595eb6188bbf6fe4e9c48ed77cb17acf4e80 updated; diff -r 2f5f595eb618 -r ab7954ba5261 src/HOL/Import/HOL/bool.imp --- a/src/HOL/Import/HOL/bool.imp Mon Sep 26 19:19:14 2005 +0200 +++ b/src/HOL/Import/HOL/bool.imp Mon Sep 26 19:19:15 2005 +0200 @@ -37,7 +37,7 @@ "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" + "bool_INDUCT" > "Datatype.bool.induct_correctness" "boolAxiom" > "HOL4Base.bool.boolAxiom" "UNWIND_THM2" > "HOL.simp_thms_39" "UNWIND_THM1" > "HOL.simp_thms_40" diff -r 2f5f595eb618 -r ab7954ba5261 src/HOL/Import/HOL/pair.imp --- a/src/HOL/Import/HOL/pair.imp Mon Sep 26 19:19:14 2005 +0200 +++ b/src/HOL/Import/HOL/pair.imp Mon Sep 26 19:19:15 2005 +0200 @@ -21,7 +21,7 @@ "##" > "prod_fun" thm_maps - "pair_induction" > "Datatype.prod.induct" + "pair_induction" > "Datatype.prod.induct_correctness" "pair_case_thm" > "Product_Type.split" "pair_case_def" > "HOL4Compat.pair_case_def" "pair_case_cong" > "HOL4Base.pair.pair_case_cong"