--- a/src/HOL/Dense_Linear_Order.thy Sun Jul 22 22:01:30 2007 +0200
+++ b/src/HOL/Dense_Linear_Order.thy Sun Jul 22 23:23:39 2007 +0200
@@ -146,7 +146,7 @@
lemma "\<forall>(a::'a::ordered_field) b. (\<exists>x. a < x \<and> x< b) \<longleftrightarrow> (a < b)"
by dlo
-section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see Arith_Tools.thy *}
+section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
context Linorder
begin