# HG changeset patch
# User nipkow
# Date 1084348856 -7200
# Node ID c8e1937110c2fc58397c2bde203e15d2682a22a3
# Parent  86c6f272ef794074ea8ea59e9071b7a546a4d6c7
fixed latex problems

diff -r 86c6f272ef79 -r c8e1937110c2 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed May 12 08:14:29 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Wed May 12 10:00:56 2004 +0200
@@ -892,7 +892,7 @@
 
 lemma setsum_constant_nat [simp]:
     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
-  -- {* Later generalized to any comm_semiring_1_cancel. *}
+  -- {* Later generalized to any @{text comm_semiring_1_cancel}. *}
   by (erule finite_induct, auto)
 
 lemma setsum_Un: "finite A ==> finite B ==>
diff -r 86c6f272ef79 -r c8e1937110c2 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed May 12 08:14:29 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed May 12 10:00:56 2004 +0200
@@ -235,7 +235,7 @@
 by (rule trans [OF zmult_commute zmult_1])
 
 
-text{*The Integers Form A comm_ring_1*}
+text{*The integers form a @{text comm_ring_1}*}
 instance int :: comm_ring_1
 proof
   fix i j k :: int
@@ -368,7 +368,7 @@
     zabs_def:  "abs(i::int) == if i < 0 then -i else i"
 
 
-text{*The Integers Form an Ordered comm_ring_1*}
+text{*The integers form an ordered @{text comm_ring_1}*}
 instance int :: ordered_idom
 proof
   fix i j k :: int
@@ -560,7 +560,8 @@
 by (simp add: linorder_not_less neg_def)
 
 
-subsection{*Embedding of the Naturals into any comm_semiring_1_cancel: @{term of_nat}*}
+subsection{*Embedding of the Naturals into any @{text
+comm_semiring_1_cancel}: @{term of_nat}*}
 
 consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
 
@@ -616,8 +617,9 @@
 declare of_nat_le_iff [of 0, simplified, simp]
 declare of_nat_le_iff [of _ 0, simplified, simp]
 
-text{*The ordering on the comm_semiring_1_cancel is necessary to exclude the possibility of
-a finite field, which indeed wraps back to zero.*}
+text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
+to exclude the possibility of a finite field, which indeed wraps back to
+zero.*}
 lemma of_nat_eq_iff [simp]:
      "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
 by (simp add: order_eq_iff)
@@ -681,7 +683,8 @@
 qed
 
 
-subsection{*Embedding of the Integers into any comm_ring_1: @{term of_int}*}
+subsection{*Embedding of the Integers into any @{text comm_ring_1}:
+@{term of_int}*}
 
 constdefs
    of_int :: "int => 'a::comm_ring_1"
@@ -738,7 +741,8 @@
 declare of_int_less_iff [of 0, simplified, simp]
 declare of_int_less_iff [of _ 0, simplified, simp]
 
-text{*The ordering on the comm_ring_1 is necessary. See @{text of_nat_eq_iff} above.*}
+text{*The ordering on the @{text comm_ring_1} is necessary.
+ See @{text of_nat_eq_iff} above.*}
 lemma of_int_eq_iff [simp]:
      "(of_int w = (of_int z::'a::ordered_idom)) = (w = z)"
 by (simp add: order_eq_iff)
diff -r 86c6f272ef79 -r c8e1937110c2 src/HOL/Nat.thy
--- 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