Wed, 02 Jan 2008 15:14:17 +0100 |
haftmann |
removed some legacy instantiations
|
file |
diff |
annotate
|
Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
Tue, 06 Nov 2007 08:47:25 +0100 |
haftmann |
renamed lordered_*_* to lordered_*_add_*; further localization
|
file |
diff |
annotate
|
Fri, 20 Jul 2007 14:28:01 +0200 |
haftmann |
split class abs from class minus
|
file |
diff |
annotate
|
Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
Fri, 16 Mar 2007 21:32:08 +0100 |
haftmann |
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
|
file |
diff |
annotate
|
Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
Sun, 12 Nov 2006 19:22:10 +0100 |
nipkow |
started reorgnization of lattice theories
|
file |
diff |
annotate
|
Wed, 20 Sep 2006 00:24:24 +0200 |
wenzelm |
renamed axclass_xxxx axclasses;
|
file |
diff |
annotate
|
Wed, 19 Oct 2005 21:52:27 +0200 |
wenzelm |
isatool fixheaders;
|
file |
diff |
annotate
|
Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
Fri, 03 Sep 2004 17:10:36 +0200 |
obua |
Matrix theory, linear programming
|
file |
diff |
annotate
|
Mon, 14 Jun 2004 14:20:55 +0200 |
obua |
Further development of matrix theory
|
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 17:10:41 +0200 |
obua |
preparation for integration with new Ring_and_Field.thy
|
file |
diff |
annotate
|
Sat, 01 May 2004 22:01:57 +0200 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
Fri, 23 Apr 2004 20:49:26 +0200 |
wenzelm |
proper document setup;
|
file |
diff |
annotate
|
Fri, 16 Apr 2004 18:30:51 +0200 |
obua |
first version of matrices for HOL/Isabelle
|
file |
diff |
annotate
|