diff -r 15d76ed6ea67 -r 1a65b780bd56 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Feb 25 14:25:52 2011 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Feb 25 20:07:48 2011 +0100
@@ -277,10 +277,7 @@
 end
 
 (* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
-lemma dnf[no_atp]:
-  "(P & (Q | R)) = ((P&Q) | (P&R))" 
-  "((Q | R) & P) = ((Q&P) | (R&P))"
-  by blast+
+lemmas dnf[no_atp] = conj_disj_distribL conj_disj_distribR
 
 lemmas weak_dnf_simps[no_atp] = simp_thms dnf
 
@@ -875,7 +872,7 @@
   {isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss}
 end
 *}
-
+(*
 lemma upper_bound_finite_set:
   assumes fS: "finite S"
   shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> a"
@@ -927,7 +924,6 @@
   hence ?thesis by blast}
 ultimately show ?thesis by blast
 qed
-
-
+*)
 
 end