# HG changeset patch
# User haftmann
# Date 1170255910 -3600
# Node ID 30a8890d29671a61c1e048537b517aff6b2a0dd9
# Parent  a5d983f7113f31712d2adae7d52ffdca4644cabe
dropped lemma duplicates in HOL.thy

diff -r a5d983f7113f -r 30a8890d2967 NEWS
--- a/NEWS	Wed Jan 31 14:03:31 2007 +0100
+++ b/NEWS	Wed Jan 31 16:05:10 2007 +0100
@@ -507,11 +507,17 @@
 
 *** HOL ***
 
+* Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq.
+INCOMPATIBILITY.
+
+* Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj.
+INCOMPATIBILITY.
+
 * Added syntactic class "size"; overloaded constant "size" now has
 type "'a::size ==> bool"
 
 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
-dvd" to "Divides.div", "Divides.mod" and
+dvd" to "Divides.div", "Divides.mod" and "Divides.dvd"
 "Divides.dvd". INCOMPATIBILITY.
 
 * Added method "lexicographic_order" automatically synthesizes
diff -r a5d983f7113f -r 30a8890d2967 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/Bali/Evaln.thy	Wed Jan 31 16:05:10 2007 +0100
@@ -191,7 +191,7 @@
           \<Longrightarrow>
 		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
 monos
-  if_def2
+  if_bool_eq_conj
 
 
 declare split_if     [split del] split_if_asm     [split del]
diff -r a5d983f7113f -r 30a8890d2967 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/HOL.ML	Wed Jan 31 16:05:10 2007 +0100
@@ -14,7 +14,6 @@
 val cong = thm "cong"
 val conj_comms = thms "conj_comms";
 val conj_cong = thm "conj_cong";
-val def_imp_eq = thm "def_imp_eq";
 val de_Morgan_conj = thm "de_Morgan_conj";
 val de_Morgan_disj = thm "de_Morgan_disj";
 val disj_assoc = thm "disj_assoc";
diff -r a5d983f7113f -r 30a8890d2967 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/HOL.thy	Wed Jan 31 16:05:10 2007 +0100
@@ -249,12 +249,6 @@
 lemma trans: "[| r=s; s=t |] ==> r=t"
   by (erule subst)
 
-lemma def_imp_eq:
-  assumes meq: "A == B"
-  shows "A = B"
-  by (unfold meq) (rule refl)
-
-(*a mere copy*)
 lemma meta_eq_to_obj_eq: 
   assumes meq: "A == B"
   shows "A = B"
@@ -818,7 +812,7 @@
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
   val eq_reflection = @{thm HOL.eq_reflection}
-  val rev_eq_reflection = @{thm HOL.def_imp_eq}
+  val rev_eq_reflection = @{thm HOL.meta_eq_to_obj_eq}
   val imp_intr = @{thm HOL.impI}
   val rev_mp = @{thm HOL.rev_mp}
   val subst = @{thm HOL.subst}
@@ -1381,9 +1375,6 @@
 
 subsection {* Other simple lemmas and lemma duplicates *}
 
-lemmas eq_sym_conv = eq_commute
-lemmas if_def2 = if_bool_eq_conj
-
 lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x"
   by blast+
 
@@ -1410,6 +1401,8 @@
   shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
 
+lemmas eq_sym_conv = eq_commute
+
 
 subsection {* Basic ML bindings *}
 
diff -r a5d983f7113f -r 30a8890d2967 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/Inductive.thy	Wed Jan 31 16:05:10 2007 +0100
@@ -64,7 +64,7 @@
 setup OldInductivePackage.setup
 
 theorems basic_monos [mono] =
-  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_def2
+  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   Collect_mono in_mono vimage_mono
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
   not_all not_ex
@@ -75,7 +75,7 @@
 setup InductivePackage.setup
 
 theorems [mono2] =
-  imp_refl disj_mono conj_mono ex_mono all_mono if_def2
+  imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
   not_all not_ex
   Ball_def Bex_def
diff -r a5d983f7113f -r 30a8890d2967 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/Integ/NatBin.thy	Wed Jan 31 16:05:10 2007 +0100
@@ -823,7 +823,7 @@
   "neg ((number_of Numeral.Min) \<Colon> int)"
   by auto
 
-lemmas nat_number_expand = nat_number Let_def if_def2 if_True if_False
+lemmas nat_number_expand = nat_number Let_def if_bool_eq_conj if_True if_False
   neg_number_of_Pls neg_number_of_Min neg_number_of_BIT Nat.plus.simps
 
 ML {*
diff -r a5d983f7113f -r 30a8890d2967 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jan 31 16:05:10 2007 +0100
@@ -176,7 +176,8 @@
 
 (*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
   where some types have the empty sort.*)
-fun mk_object_eq th = th RS def_imp_eq
+val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
+fun mk_object_eq th = th RS meta_eq_to_obj_eq
     handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
 
 (*Apply a function definition to an argument, beta-reducing the result.*)