# HG changeset patch
# User haftmann
# Date 1208845999 -7200
# Node ID 47224a933c144a8ac7545fc6cfd67176835ee1f5
# Parent  6ea9de67e57659eae6e54cd316706d23cb5dddf0
tuned proofs

diff -r 6ea9de67e576 -r 47224a933c14 src/HOL/Dense_Linear_Order.thy
--- a/src/HOL/Dense_Linear_Order.thy	Tue Apr 22 08:33:16 2008 +0200
+++ b/src/HOL/Dense_Linear_Order.thy	Tue Apr 22 08:33:19 2008 +0200
@@ -264,7 +264,7 @@
 lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
   le_less neq_iff linear less_not_permute
 
-lemma axiom: "dense_linear_order (op \<le>) (op <)" by fact
+lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
 lemma atoms:
   includes meta_term_syntax
   shows "TERM (less :: 'a \<Rightarrow> _)"
@@ -500,7 +500,8 @@
 lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
 lemmas lin_dense_thms = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
 
-lemma ferrack_axiom: "constr_dense_linear_order less_eq less between" by fact
+lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
+  by (rule constr_dense_linear_order_axioms)
 lemma atoms:
   includes meta_term_syntax
   shows "TERM (less :: 'a \<Rightarrow> _)"