| Mon, 09 Jun 2008 17:07:08 +0200 |
wenzelm |
adapted case_tac/induct_tac;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 12:09:33 +0200 |
chaieb |
fixed proofs
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
| Sat, 21 Jul 2007 23:25:00 +0200 |
wenzelm |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
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
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 06 Jun 2005 13:30:21 +0200 |
nipkow |
junk
|
file |
diff |
annotate
|
| Mon, 02 May 2005 19:00:05 +0200 |
nipkow |
fixed
|
file |
diff |
annotate
|
| Wed, 02 Mar 2005 12:06:15 +0100 |
nipkow |
another reorganization of setsums and intervals
|
file |
diff |
annotate
|
| Thu, 15 Jul 2004 13:11:34 +0200 |
nipkow |
Moved to new m<..<n syntax for set intervals.
|
file |
diff |
annotate
|
| Wed, 14 Jul 2004 10:25:21 +0200 |
nipkow |
?
|
file |
diff |
annotate
|
| Tue, 13 Jul 2004 12:32:01 +0200 |
nipkow |
Got rid of Summation and made it a translation into setsum instead.
|
file |
diff |
annotate
|
| Wed, 19 May 2004 11:21:19 +0200 |
chaieb |
tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:14:02 +0200 |
berghofe |
Adapted to new simplifier.
|
file |
diff |
annotate
|
| Fri, 23 Aug 2002 07:41:05 +0200 |
nipkow |
Added div+mod cancelling simproc
|
file |
diff |
annotate
|
| Thu, 30 May 2002 10:12:52 +0200 |
nipkow |
Modifications due to enhanced linear arithmetic.
|
file |
diff |
annotate
|
| Tue, 05 Mar 2002 18:19:11 +0100 |
prensani |
New order in the loading of theories (Quote-antiquote right before the OG_Syntax and RG_Syntax respectively)
|
file |
diff |
annotate
|
| Tue, 05 Mar 2002 17:11:25 +0100 |
prensani |
HoareParallel Theories
|
file |
diff |
annotate
|