# HG changeset patch
# User haftmann
# Date 1193742864 -3600
# Node ID ee73d4c33a88bab53d8fdb29b23824bd9a344065
# Parent  5dbb6d583adc118848bf8183fa7ea779454ad115
fixed document preparation

diff -r 5dbb6d583adc -r ee73d4c33a88 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Oct 30 12:14:23 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Oct 30 12:14:24 2007 +0100
@@ -520,8 +520,8 @@
 
 class ordered_ring = ring + ordered_semiring
   + lordered_ab_group + abs_if
-  -- {*FIXME: should inherit from ordered_ab_group_add rather than
-         lordered_ab_group*}
+  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
+         @{text lordered_ab_group}*}
 
 instance ordered_ring \<subseteq> lordered_ring
 proof 
@@ -535,8 +535,8 @@
  *)
 class ordered_ring_strict = ring + ordered_semiring_strict
   + lordered_ab_group + abs_if
-  -- {*FIXME: should inherit from ordered_ab_group_add rather than
-         lordered_ab_group*}
+  -- {*FIXME: should inherit from @{text ordered_ab_group_add} rather than
+         @{text lordered_ab_group}*}
 
 instance ordered_ring_strict \<subseteq> ordered_ring by intro_classes