| Mon, 17 Oct 2005 23:10:15 +0200 |
wenzelm |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 16:59:48 +0200 |
wenzelm |
axclass: name space prefix is now "c_class" instead of just "c";
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:26 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 23 May 2005 19:39:45 +0200 |
nipkow |
tuned setsum rewrites
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:32:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Fri, 05 Mar 2004 15:30:49 +0100 |
paulson |
tweaked for times_ac1
|
file |
diff |
annotate
|
| Thu, 23 Jan 2003 09:16:53 +0100 |
ballarin |
Fixed term order for normal form in rings.
|
file |
diff |
annotate
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 20:34:12 +0200 |
wenzelm |
ring includes plus_ac0;
|
file |
diff |
annotate
|
| Sat, 10 Feb 2001 08:52:41 +0100 |
ballarin |
Changes to HOL/Algebra:
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:15:14 +0100 |
wenzelm |
use inverse, divide from basic HOL;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2000 12:28:32 +0200 |
paulson |
renamed // to / (which is what we want anyway) to avoid clash with the new
|
file |
diff |
annotate
|
| Fri, 05 Nov 1999 11:14:26 +0100 |
paulson |
Algebra and Polynomial theories, by Clemens Ballarin
|
file |
diff |
annotate
|