# HG changeset patch
# User nipkow
# Date 1089991904 -7200
# Node ID 405be2b48f5bb5b9d8a67e62f239cdbe7cdd0ffd
# Parent  cc562a263609747562efcb545da0537a7ec1e465
Corrected TeX problems.

diff -r cc562a263609 -r 405be2b48f5b src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Fri Jul 16 11:46:59 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Fri Jul 16 17:31:44 2004 +0200
@@ -280,7 +280,7 @@
 declare hypnat_zero_not_eq_one [THEN not_sym, simp]
 
 
-text{*The Hypernaturals Form A comm_semiring_1_cancel*}
+text{*The hypernaturals form a @{text comm_semiring_1_cancel}: *}
 instance hypnat :: comm_semiring_1_cancel
 proof
   fix i j k :: hypnat
@@ -349,7 +349,7 @@
 done
 
 
-subsection{*The Hypernaturals Form an Ordered comm_semiring_1_cancel*}
+subsection{*The Hypernaturals Form an Ordered @{text comm_semiring_1_cancel} *}
 
 instance hypnat :: ordered_semidom
 proof
@@ -453,8 +453,8 @@
 qed
 
 
-subsection{*The Embedding @{term hypnat_of_nat} Preserves comm_ring_1 and 
-      Order Properties*}
+subsection{*The Embedding @{term hypnat_of_nat} Preserves @{text
+comm_ring_1} and Order Properties*}
 
 constdefs
 
diff -r cc562a263609 -r 405be2b48f5b src/HOL/Hyperreal/Log.thy
--- a/src/HOL/Hyperreal/Log.thy	Fri Jul 16 11:46:59 2004 +0200
+++ b/src/HOL/Hyperreal/Log.thy	Fri Jul 16 17:31:44 2004 +0200
@@ -14,7 +14,7 @@
     "x powr a == exp(a * ln x)"
 
   log :: "[real,real] => real"
-    --{*logarithm of @[term x} to base @[term a}*}
+    --{*logarithm of @{term x} to base @{term a}*}
     "log a x == ln x / ln a"
 
 
diff -r cc562a263609 -r 405be2b48f5b src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Fri Jul 16 11:46:59 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Fri Jul 16 17:31:44 2004 +0200
@@ -24,10 +24,6 @@
    "suminf f == (@s. f sums s)"
 
 
-text{*This simprule replaces @{text "sumr 0 n"} by a term involving 
-  @{term lessThan}, making other simprules inapplicable.*}
-declare atLeast0LessThan [simp del]
-
 lemma sumr_Suc [simp]:
      "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
 by (simp add: atLeastLessThanSuc)
diff -r cc562a263609 -r 405be2b48f5b src/HOL/Hyperreal/Transcendental.ML
--- a/src/HOL/Hyperreal/Transcendental.ML	Fri Jul 16 11:46:59 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.ML	Fri Jul 16 17:31:44 2004 +0200
@@ -394,8 +394,6 @@
 (* Properties of power series                                               *)
 (*--------------------------------------------------------------------------*)
 
-Delsimps [thm"atLeast0LessThan"];
-
 Goal "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) = \
 \     y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))";
 by (auto_tac (claset(),simpset() addsimps [sumr_mult] delsimps [sumr_Suc]));