| 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
|