--- 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
--- 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]
--- 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";
--- 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 *}
--- 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
--- 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 {*
--- 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.*)