| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 14:55:10 +0200 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 12:40:08 +0200 |
wenzelm |
modernized some specifications;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:56:32 +0100 |
haftmann |
dropped odd interpretation of comm_monoid_mult into comm_monoid_add
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 15:34:29 +0100 |
wenzelm |
eliminated old-style prems;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:06:41 +0100 |
haftmann |
separate library theory for type classes combining lattices with various algebraic structures
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Mon, 11 Jan 2010 11:47:38 +0100 |
hoelzl |
Matrices form a semiring with 0
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2009 16:25:44 +0200 |
wenzelm |
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 19:49:05 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 31 Jan 2009 09:04:16 +0100 |
nipkow |
added some simp rules
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Fri, 17 Oct 2008 10:39:39 +0200 |
wenzelm |
reactivated HOL-Matrix;
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:57 +0200 |
haftmann |
more class instantiations
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 19:20:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 04 Jul 2008 07:39:01 +0200 |
haftmann |
added marginal setup for code generation
|
file |
diff |
annotate
|
| 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
|