| Thu, 23 Nov 2006 22:38:29 +0100 |
wenzelm |
prefer Proof.context over Context.generic;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 08:18:59 +0200 |
haftmann |
abandoned equal_list in favor for eq_list
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 19:25:58 +0200 |
ballarin |
Reimplemented algebra method; now controlled by attribute.
|
file |
diff |
annotate
|
| Fri, 14 Jul 2006 14:37:15 +0200 |
ballarin |
Term.term_lpo takes order on terms rather than strings as argument.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Sat, 25 Jun 2005 16:06:17 +0200 |
nipkow |
Changes due to new abel_cancel.ML
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:13:59 +0200 |
wenzelm |
get_thm(s): Name;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 18:16:57 +0100 |
berghofe |
Adapted to modified interface of PureThy.get_thm(s).
|
file |
diff |
annotate
|
| Thu, 17 Jun 2004 17:18:30 +0200 |
paulson |
removal of magmas and semigroups
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 16:44:21 +0100 |
ballarin |
New lemmas about inversion of restricted functions.
|
file |
diff |
annotate
|
| Wed, 30 Apr 2003 10:01:35 +0200 |
ballarin |
Greatly extended CRing. Added Module.
|
file |
diff |
annotate
|
| Fri, 14 Mar 2003 18:00:16 +0100 |
ballarin |
Bugs fixed and operators finprod and finsum.
|
file |
diff |
annotate
|
| Mon, 10 Mar 2003 17:25:34 +0100 |
ballarin |
First distributed version of Group and Ring theory.
|
file |
diff |
annotate
|