summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Groups.thy

changeset 70347 | e5cd5471c18a |

parent 69605 | a96320074298 |

1.1 --- a/src/HOL/Groups.thy Fri Jun 14 08:34:28 2019 +0000 1.2 +++ b/src/HOL/Groups.thy Fri Jun 14 08:34:28 2019 +0000 1.3 @@ -15,8 +15,9 @@ 1.4 subsection \<open>Dynamic facts\<close> 1.5 1.6 named_theorems ac_simps "associativity and commutativity simplification rules" 1.7 - and algebra_simps "algebra simplification rules" 1.8 + and algebra_simps "algebra simplification rules for rings" 1.9 and field_simps "algebra simplification rules for fields" 1.10 + and sign_simps "algebra simplification rules for comparision with zero" 1.11 1.12 text \<open> 1.13 The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical 1.14 @@ -32,6 +33,10 @@ 1.15 can be proved to be non-zero (for equations) or positive/negative (for 1.16 inequalities). Can be too aggressive and is therefore separate from the more 1.17 benign \<open>algebra_simps\<close>. 1.18 + 1.19 + Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs 1.20 + of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> 1.21 + because the former can lead to case explosions. 1.22 \<close> 1.23 1.24