| Sat, 29 Aug 2009 12:01:25 +0200 |
eliminated hard tabs;
|
file | diff | annotate |
| Wed, 15 Jul 2009 23:48:21 +0200 |
more antiquotations;
|
file | diff | annotate |
| Mon, 27 Apr 2009 10:11:44 +0200 |
cleaned up theory power further
|
file | diff | annotate |
| Thu, 23 Apr 2009 12:17:51 +0200 |
adaptions due to rearrangment of power operation
|
file | diff | annotate |
| Mon, 16 Mar 2009 18:24:30 +0100 |
simplified method setup;
|
file | diff | annotate |
| Fri, 13 Mar 2009 19:58:26 +0100 |
unified type Proof.method and pervasive METHOD combinators;
|
file | diff | annotate |
| Wed, 28 Jan 2009 16:57:36 +0100 |
merged
|
file | diff | annotate |
| Wed, 28 Jan 2009 16:29:16 +0100 |
Replaced group_ and ring_simps by algebra_simps;
|
file | diff | annotate |
| Wed, 28 Jan 2009 16:35:42 +0100 |
explicit check for exactly one type variable in class specification elements
|
file | diff | annotate |
| Wed, 31 Dec 2008 15:30:10 +0100 |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file | diff | annotate |
| Fri, 18 Jul 2008 18:25:53 +0200 |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file | diff | annotate |
| Fri, 11 Jul 2008 09:02:24 +0200 |
class instead of axclass
|
file | diff | annotate |
| Sat, 29 Mar 2008 19:14:00 +0100 |
replaced 'ML_setup' by 'ML';
|
file | diff | annotate |
| Wed, 19 Mar 2008 22:50:42 +0100 |
more antiquotations;
|
file | diff | annotate |
| Wed, 02 Jan 2008 15:14:02 +0100 |
splitted class uminus from class minus
|
file | diff | annotate |
| Fri, 12 Oct 2007 08:20:46 +0200 |
class div inherits from class times
|
file | diff | annotate |
| Sat, 21 Jul 2007 23:25:00 +0200 |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
file | diff | annotate |
| Thu, 17 May 2007 19:49:40 +0200 |
canonical prefixing of class constants
|
file | diff | annotate |
| Thu, 26 Apr 2007 14:24:08 +0200 |
eliminated unnamed infixes, tuned syntax;
|
file | diff | annotate |
| Fri, 02 Mar 2007 15:43:15 +0100 |
prefix of class interpretation not mandatory any longer
|
file | diff | annotate |
| Wed, 29 Nov 2006 15:44:51 +0100 |
simplified method setup;
|
file | diff | annotate |
| Sun, 19 Nov 2006 23:48:55 +0100 |
HOL-Algebra: converted legacy ML scripts;
|
file | diff | annotate |
| Sat, 18 Nov 2006 00:20:24 +0100 |
dvd_def now with object equality
|
file | diff | annotate |
| Thu, 03 Aug 2006 14:57:26 +0200 |
Restructured algebra library, added ideals and quotient rings.
|
file | diff | annotate |