| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 05:18:39 +0200 |
huffman |
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 03:31:11 +0200 |
huffman |
removed constant int :: nat => int;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2006 10:42:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 19:40:13 +0100 |
wenzelm |
tuned specifications;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:19:51 +0200 |
wenzelm |
attribute symmetric: zero_var_indexes;
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 03:19:08 +0200 |
webertj |
lin_arith_prover: splitting reverted because of performance loss
|
file |
diff |
annotate
|
| Mon, 07 Aug 2006 03:10:38 +0200 |
webertj |
title fixed
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Wed, 17 May 2006 01:23:41 +0200 |
wenzelm |
prefer 'definition' over low-level defs;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 12:50:04 +0100 |
wenzelm |
tuned sources and proofs
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 17:41:10 +0200 |
nipkow |
prime is a predicate now.
|
file |
diff |
annotate
|