| Tue, 03 Jul 2007 18:42:09 +0200 |
huffman |
convert instance proofs to Isar style
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:28:36 +0200 |
huffman |
rename class dom to ring_1_no_zero_divisors
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 01:26:06 +0200 |
huffman |
instance pordered_comm_ring < pordered_ring
|
file |
diff |
annotate
|
| Sat, 30 Jun 2007 17:30:10 +0200 |
obua |
added ordered_ring and ordered_semiring
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 15:19:18 +0200 |
nipkow |
removed redundant lemmas
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 21:15:55 +0200 |
nipkow |
tex problem fixed
|
file |
diff |
annotate
|
| Sun, 24 Jun 2007 20:55:41 +0200 |
nipkow |
tuned and used field_simps
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 18:47:03 +0200 |
nipkow |
tuned laws for cancellation in divisions for fields.
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 13:39:29 +0200 |
chaieb |
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
|
file |
diff |
annotate
|
| Sat, 16 Jun 2007 15:01:54 +0200 |
nipkow |
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
|
file |
diff |
annotate
|
| Fri, 15 Jun 2007 15:10:32 +0200 |
nipkow |
made divide_self a simp rule
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 16:21:03 +0200 |
nipkow |
hid constant "dom"
|
file |
diff |
annotate
|
| Thu, 24 May 2007 16:52:54 +0200 |
obua |
Squared things out.
|
file |
diff |
annotate
|