--- 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