Sun, 21 Mar 2010 17:12:31 +0100 |
wenzelm |
standard headers;
|
file |
diff |
annotate
|
Thu, 23 Apr 2009 12:17:51 +0200 |
haftmann |
adaptions due to rearrangment of power operation
|
file |
diff |
annotate
|
Sat, 14 Jun 2008 23:20:06 +0200 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
Wed, 19 Mar 2008 22:50:42 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Thu, 27 Sep 2007 17:55:28 +0200 |
paulson |
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
|
file |
diff |
annotate
|
Fri, 02 Mar 2007 15:43:15 +0100 |
haftmann |
prefix of class interpretation not mandatory any longer
|
file |
diff |
annotate
|
Sun, 19 Nov 2006 23:48:55 +0100 |
wenzelm |
HOL-Algebra: converted legacy ML scripts;
|
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
|
Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
Mon, 10 May 2004 16:40:54 +0200 |
obua |
moved first lemma in LongDiv.ML to LongDiv.thy
|
file |
diff |
annotate
|
Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
Sat, 10 Feb 2001 08:52:41 +0100 |
ballarin |
Changes to HOL/Algebra:
|
file |
diff |
annotate
|
Fri, 05 Nov 1999 11:14:26 +0100 |
paulson |
Algebra and Polynomial theories, by Clemens Ballarin
|
file |
diff |
annotate
|