# 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. *}