--- a/src/HOL/Nat.thy Wed May 12 08:14:29 2004 +0200
+++ b/src/HOL/Nat.thy Wed May 12 10:00:56 2004 +0200
@@ -712,7 +712,7 @@
by (induct m) (simp_all add: add_mult_distrib)
-text{*The Naturals Form A comm_semiring_1_cancel*}
+text{*The naturals form a @{text comm_semiring_1_cancel}*}
instance nat :: comm_semiring_1_cancel
proof
fix i j k :: nat
@@ -760,7 +760,7 @@
done
-text{*The Naturals Form an Ordered comm_semiring_1_cancel*}
+text{*The naturals form an ordered @{text comm_semiring_1_cancel}*}
instance nat :: ordered_semidom
proof
fix i j k :: nat