# HG changeset patch
# User wenzelm
# Date 1128009672 -7200
# Node ID 83d64a4615075295141d20899f4e47aefb80f6e4
# Parent  957c1fd897da2c219204e28d1454a6987fea4032
updated;

diff -r 957c1fd897da -r 83d64a461507 src/HOL/Import/HOL/HOL4Base.thy
--- a/src/HOL/Import/HOL/HOL4Base.thy	Thu Sep 29 17:09:11 2005 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy	Thu Sep 29 18:01:12 2005 +0200
@@ -1469,9 +1469,6 @@
 lemma LESS_EQUAL_ADD: "ALL (m::nat) n::nat. m <= n --> (EX p::nat. n = m + p)"
   by (import arithmetic LESS_EQUAL_ADD)
 
-lemma LESS_EQ_EXISTS: "ALL (m::nat) n::nat. (m <= n) = (EX p::nat. n = m + p)"
-  by (import arithmetic LESS_EQ_EXISTS)
-
 lemma MULT_EQ_1: "ALL (x::nat) y::nat. (x * y = 1) = (x = 1 & y = 1)"
   by (import arithmetic MULT_EQ_1)
 
diff -r 957c1fd897da -r 83d64a461507 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Thu Sep 29 17:09:11 2005 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp	Thu Sep 29 18:01:12 2005 +0200
@@ -185,7 +185,7 @@
   "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
   "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
   "LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc"
-  "LESS_EQ_EXISTS" > "HOL4Base.arithmetic.LESS_EQ_EXISTS"
+  "LESS_EQ_EXISTS" > "NatArith.le_iff_add"
   "LESS_EQ_CASES" > "Nat.nat_le_linear"
   "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
   "LESS_EQ_ADD_SUB" > "NatArith.add_diff_assoc"
diff -r 957c1fd897da -r 83d64a461507 src/HOL/Import/HOL/bool.imp
--- a/src/HOL/Import/HOL/bool.imp	Thu Sep 29 17:09:11 2005 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Thu Sep 29 18:01:12 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 957c1fd897da -r 83d64a461507 src/HOL/Import/HOL/pair.imp
--- a/src/HOL/Import/HOL/pair.imp	Thu Sep 29 17:09:11 2005 +0200
+++ b/src/HOL/Import/HOL/pair.imp	Thu Sep 29 18:01:12 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"