| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Thu, 02 Aug 2007 18:13:42 +0200 |
ballarin |
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:29:57 +0200 |
ballarin |
Interpretation of rings (as integers) maps defined operations to defined
|
file |
diff |
annotate
|
| Fri, 12 Jan 2007 15:37:21 +0100 |
ballarin |
Reverted to structure representation with records.
|
file |
diff |
annotate
|
| Fri, 22 Dec 2006 14:03:30 +0100 |
ballarin |
Experimenting with interpretations of "definition".
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 10:27:54 +0200 |
ballarin |
Order and lattice structures no longer based on records.
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|