| Mon, 11 Jun 2007 11:06:19 +0200 |
chaieb |
A new tactic for Presburger;
|
file |
diff |
annotate
|
| Mon, 04 Jun 2007 09:57:02 +0200 |
chaieb |
tuned;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 13:00:56 +0200 |
wenzelm |
fixed title;
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:40 +0200 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:09 +0200 |
haftmann |
slightly tuned
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:03 +0200 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
| Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:24 +0100 |
haftmann |
dvd_def now with object equality
|
file |
diff |
annotate
|
| Wed, 04 Oct 2006 14:17:38 +0200 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Fri, 25 Aug 2006 00:10:10 +0200 |
webertj |
avoid duplicate tactics
|
file |
diff |
annotate
|
| Thu, 24 Aug 2006 23:51:46 +0200 |
webertj |
additional list of tactics that can be added to arith
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 02:06:01 +0200 |
webertj |
bugfix related to cancel_div_mod simproc
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:00 +0200 |
wenzelm |
renamed Term.variant_abs to Syntax.variant_abs;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:41 +0200 |
wenzelm |
presburger_ss: proper context;
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 09:34:23 +0100 |
haftmann |
renamed op < <= to Orderings.less(_eq)
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 16:24:12 +0100 |
chaieb |
deals with Suc in mod expressions
|
file |
diff |
annotate
|
| Fri, 18 Nov 2005 07:13:58 +0100 |
chaieb |
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
|
file |
diff |
annotate
|
| Fri, 11 Nov 2005 10:49:59 +0100 |
chaieb |
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:25 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:18 +0200 |
wenzelm |
improved oracle setup;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:25:33 +0200 |
wenzelm |
reverted renaming of Some/None in comments and strings;
|
file |
diff |
annotate
|
| Wed, 23 Mar 2005 12:09:18 +0100 |
paulson |
replaced bool by a new datatype "bit" for binary numerals
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 11 Oct 2004 19:36:48 +0200 |
berghofe |
Replaced the_context() by theory "Presburger" in call of invoke_oracle.
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Mon, 14 Jun 2004 16:46:48 +0200 |
chaieb |
Oracle corrected
|
file |
diff |
annotate
|
| Sat, 12 Jun 2004 13:50:55 +0200 |
chaieb |
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
|
file |
diff |
annotate
|
| Sun, 06 Jun 2004 18:36:36 +0200 |
wenzelm |
avoid Args.list (lost update?);
|
file |
diff |
annotate
|
| Sat, 05 Jun 2004 18:34:06 +0200 |
chaieb |
More readable code.
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:09:47 +0200 |
wenzelm |
avoid Args.list;
|
file |
diff |
annotate
|
| Wed, 26 May 2004 19:06:09 +0200 |
chaieb |
abstraction over functions is no default any more.
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:49:45 +0200 |
berghofe |
- deleted unneeded function eta_long (now in Pure/pattern.ML
|
file |
diff |
annotate
|
| Wed, 19 May 2004 11:23:59 +0200 |
chaieb |
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 17:52:38 +0200 |
berghofe |
Fixed two bugs:
|
file |
diff |
annotate
|
| Sat, 10 May 2003 20:52:18 +0200 |
berghofe |
- Added split_min and split_max to preprocessor
|
file |
diff |
annotate
|
| Fri, 04 Apr 2003 17:01:12 +0200 |
berghofe |
Fixed bug in eta_long.
|
file |
diff |
annotate
|
| Tue, 25 Mar 2003 09:47:05 +0100 |
berghofe |
New decision procedure for Presburger arithmetic.
|
file |
diff |
annotate
|