author nipkow Wed, 12 May 2004 10:00:56 +0200 changeset 14740 c8e1937110c2 parent 14739 86c6f272ef79 child 14741 36582c356db7
fixed latex problems
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions src/HOL/Nat.thy file | annotate | diff | comparison | revisions
```--- 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 ==>```
```--- 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 @@

-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)"
@@ -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)"
```--- 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 @@

-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```