src/HOL/Ring_and_Field.thy
changeset 23483 a9356b40fbd3
parent 23482 2f4be6844f7c
child 23496 84e9216a6d0e
--- 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. *}