| Sat, 03 Sep 2011 09:12:19 -0700 |
huffman |
simplify proof
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 09:52:09 -0700 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
file |
diff |
annotate
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
add divide_.._cancel, inverse_.._iff
|
file |
diff |
annotate
|
| Sat, 08 May 2010 17:06:58 -0700 |
huffman |
add lemmas one_less_inverse and one_le_inverse
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:11:56 +0200 |
haftmann |
moved some lemmas from Groebner_Basis here
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 12:20:17 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 11:52:41 +0200 |
haftmann |
got rid of [simplified]
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 09:49:36 +0200 |
haftmann |
tuned class linordered_field_inverse_zero
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:37:50 +0200 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:15 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 08:25:34 +0200 |
haftmann |
field_simps as named theorems
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 15:17:59 +0200 |
haftmann |
less special treatment of times_divide_eq [simp]
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 13:58:14 +0200 |
haftmann |
more localization; factored out lemmas for division_ring
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 18:42:39 +0100 |
hoelzl |
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:02 +0100 |
haftmann |
moved lemma field_le_epsilon from Real.thy to Fields.thy
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 08:49:26 +0100 |
haftmann |
moved constants inverse and divide to Ring.thy
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
| base
|