# HG changeset patch
# User wenzelm
# Date 1185139419 -7200
# Node ID fcbee3512a995523119dc73cd14413f2afdbd204
# Parent  3e0424305fa41277da467f06e1bf19f27de56deb
fixed document;

diff -r 3e0424305fa4 -r fcbee3512a99 src/HOL/Dense_Linear_Order.thy
--- 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