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
|
Tue, 22 May 2007 16:47:22 +0200 |
huffman |
add missing instance declarations
|
file |
diff |
annotate
|
Thu, 17 May 2007 19:49:16 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Thu, 17 May 2007 18:32:17 +0200 |
huffman |
added classes ring_no_zero_divisors and dom (non-commutative version of idom);
|
file |
diff |
annotate
|
Thu, 17 May 2007 08:42:51 +0200 |
huffman |
instance division_ring < no_zero_divisors; clean up field instance proofs
|
file |
diff |
annotate
|
Sun, 06 May 2007 21:49:29 +0200 |
haftmann |
added auxiliary lemmas for proof tools
|
file |
diff |
annotate
|
Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 21:32:08 +0100 |
haftmann |
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
|
file |
diff |
annotate
|
Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
Fri, 02 Mar 2007 15:43:21 +0100 |
haftmann |
now using "class"
|
file |
diff |
annotate
|
Mon, 13 Nov 2006 15:43:05 +0100 |
haftmann |
dropped Inductive dependency
|
file |
diff |
annotate
|
Thu, 09 Nov 2006 00:43:12 +0100 |
huffman |
added lemma mult_mono'
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 09:33:47 +0100 |
krauss |
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
|
file |
diff |
annotate
|
Wed, 20 Sep 2006 00:24:24 +0200 |
wenzelm |
renamed axclass_xxxx axclasses;
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 18:13:10 +0200 |
obua |
renamed axclass_xxxx axclasses
|
file |
diff |
annotate
|
Sun, 10 Sep 2006 05:34:24 +0200 |
huffman |
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
|
file |
diff |
annotate
|