# HG changeset patch
# User nipkow
# Date 1182712555 -7200
# Node ID a9356b40fbd3dc651225567cdfb70edd73d87bb7
# Parent  2f4be6844f7ca326eb8e812f18d8253ec84fe25d
tex problem fixed

diff -r 2f4be6844f7c -r a9356b40fbd3 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sun Jun 24 20:55:41 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sun Jun 24 21:15:55 2007 +0200
@@ -1523,7 +1523,7 @@
   pos_le_divide_eq neg_le_divide_eq
 
 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
-of positivity/negativity needed for field_simps. Have not added @{text
+of positivity/negativity needed for @{text field_simps}. Have not added @{text
 sign_simps} to @{text field_simps} because the former can lead to case
 explosions. *}