| Fri, 02 Apr 2004 12:08:38 +0200 |
nipkow |
Added ignore_neq flag.
|
file |
diff |
annotate
|
| Wed, 28 Jan 2004 10:41:49 +0100 |
paulson |
converted Real/Lubs to Isar script. Converting arithmetic setup
|
file |
diff |
annotate
|
| Wed, 14 Jan 2004 04:41:16 +0100 |
nipkow |
fixed old bugs in "decomp" (conversion from term to lin.arith. format).
|
file |
diff |
annotate
|
| Sat, 27 Dec 2003 21:02:14 +0100 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
| Mon, 07 Apr 2003 06:31:18 +0200 |
nipkow |
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
|
file |
diff |
annotate
|
| Tue, 25 Mar 2003 09:48:38 +0100 |
berghofe |
Added hook for presburger arithmetic decision procedure.
|
file |
diff |
annotate
|
| Fri, 23 Aug 2002 07:41:05 +0200 |
nipkow |
Added div+mod cancelling simproc
|
file |
diff |
annotate
|
| Tue, 13 Aug 2002 21:57:15 +0200 |
nipkow |
Counter example generation mods.
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2002 13:37:48 +0100 |
paulson |
Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
|
file |
diff |
annotate
|
| Mon, 25 Feb 2002 10:42:34 +0100 |
nipkow |
solved the problem that Larry's simproce cancle_numerals(?) returns
|
file |
diff |
annotate
|
| Wed, 12 Dec 2001 19:19:59 +0100 |
nipkow |
tuned conversion from terms to "polynomials" for arith_tac: takes care
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 00:46:26 +0100 |
wenzelm |
theory data: removed obsolete finish method;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2001 23:59:37 +0100 |
wenzelm |
theory data: finish method;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:02:59 +0200 |
wenzelm |
improved atomize setup;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2001 00:02:46 +0200 |
wenzelm |
* sane numerals (stage 2): plain "num" syntax (removed "#");
|
file |
diff |
annotate
|
| Fri, 05 Oct 2001 21:52:39 +0200 |
wenzelm |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 13:43:24 +0200 |
nipkow |
turned translation for 1::nat into def.
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:07:35 +0200 |
nipkow |
Allow Suc-numerals as coefficients in lin-arith formulae
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 00:28:50 +0100 |
wenzelm |
tuned atomize;
|
file |
diff |
annotate
|
| Wed, 03 Jan 2001 11:14:48 +0100 |
paulson |
removal of the nat_cancel_factor simproc
|
file |
diff |
annotate
|
| Thu, 21 Dec 2000 16:19:39 +0100 |
nipkow |
rational arithmetic
|
file |
diff |
annotate
|
| Mon, 18 Dec 2000 14:59:05 +0100 |
nipkow |
moved mk_bin from Numerals to HOLogic
|
file |
diff |
annotate
|
| Fri, 01 Dec 2000 19:53:29 +0100 |
nipkow |
Linear arithmetic now copes with mixed nat/int formulae.
|
file |
diff |
annotate
|
| Thu, 23 Nov 2000 21:33:14 +0100 |
wenzelm |
arith_tac: atomize;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:51:07 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Mon, 14 Aug 2000 14:57:29 +0200 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| Wed, 28 Oct 1998 11:25:38 +0100 |
nipkow |
added nat_diff_split and a few lemmas in Trancl.
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:23:00 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 17:17:14 +0200 |
oheimb |
renamed mk_meta_eq to mk_eq
|
file |
diff |
annotate
|
| Mon, 07 Sep 1998 10:40:17 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Tue, 01 Sep 1998 15:05:36 +0200 |
paulson |
Replaced Suc_diff_n by Suc_diff_le
|
file |
diff |
annotate
|
| Thu, 20 Aug 1998 16:44:05 +0200 |
paulson |
adjusted for new rewrites
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:14:26 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:20:49 +0200 |
oheimb |
renamed mk_meta_eq to meta_eq
|
file |
diff |
annotate
|
| Sun, 12 Jul 1998 11:49:17 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Tue, 03 Mar 1998 15:13:24 +0100 |
paulson |
New theorem
|
file |
diff |
annotate
|
| Fri, 05 Dec 1997 17:13:46 +0100 |
wenzelm |
simplification procedures nat_cancel enabled by default;
|
file |
diff |
annotate
|
| Mon, 01 Dec 1997 18:27:43 +0100 |
wenzelm |
open;
|
file |
diff |
annotate
|
| Mon, 01 Dec 1997 14:42:30 +0100 |
berghofe |
Added DiffCancelSums.
|
file |
diff |
annotate
|
| Thu, 27 Nov 1997 13:38:06 +0100 |
wenzelm |
mk_norm_sum;
|
file |
diff |
annotate
|
| Wed, 26 Nov 1997 17:52:53 +0100 |
wenzelm |
separate lists of simprocs;
|
file |
diff |
annotate
|
| Wed, 26 Nov 1997 16:44:25 +0100 |
wenzelm |
Setup various arithmetic proof procedures.
|
file |
diff |
annotate
|