| Wed, 03 Dec 2003 10:49:34 +0100 |
paulson |
Simplification of the development of Integers
|
file |
diff |
annotate
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| Thu, 20 Nov 2003 10:42:00 +0100 |
paulson |
conversion of Integ/Int_lemmas.ML to Isar script
|
file |
diff |
annotate
|
| Mon, 12 Aug 2002 17:48:19 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:46:09 +0200 |
wenzelm |
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Thu, 13 Dec 2001 15:45:03 +0100 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Fri, 02 Nov 2001 17:55:24 +0100 |
paulson |
Numerals and simprocs for types real and hypreal. The abstract
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 11:54:22 +0200 |
paulson |
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
|
file |
diff |
annotate
|
| Mon, 08 Oct 2001 15:23:20 +0200 |
wenzelm |
sane numerals (stage 3): provide generic "1" on all number types;
|
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
|
| Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2000 15:15:43 +0100 |
paulson |
coping with the re-orientation of #nn=x
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 12:39:57 +0200 |
paulson |
renamed (most of...) the select rules
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 18:47:30 +0200 |
paulson |
more integer theorems, better simplification
|
file |
diff |
annotate
|
| Thu, 17 Aug 2000 11:55:47 +0200 |
paulson |
better rules for cancellation of common factors across comparisons
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:06:46 +0200 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| Sat, 01 Jul 2000 17:52:52 +0200 |
nipkow |
Defined abs on int.
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Wed, 14 Jun 2000 17:44:43 +0200 |
paulson |
new default simprules for m*n = 0
|
file |
diff |
annotate
|
| Thu, 04 May 2000 12:29:00 +0200 |
paulson |
further tidying of integer simprocs
|
file |
diff |
annotate
|
| Wed, 03 May 2000 18:33:28 +0200 |
paulson |
Installation of CombineNumerals for the integers
|
file |
diff |
annotate
|
| Sun, 23 Apr 2000 11:34:05 +0200 |
paulson |
removed some duplication, etc.
|
file |
diff |
annotate
|
| Wed, 22 Mar 2000 13:01:18 +0100 |
paulson |
tidied using new "inst" rule
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 21:48:59 +0200 |
wenzelm |
arithmetic now in IntArith;
|
file |
diff |
annotate
|
| Thu, 23 Sep 1999 09:04:36 +0200 |
nipkow |
Restructured lin.arith.package.
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 14:13:55 +0200 |
nipkow |
Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
|
file |
diff |
annotate
|
| Wed, 08 Sep 1999 15:40:39 +0200 |
paulson |
generalized the theorem bin_add_BIT_Min to bin_add_Min_right
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 17:27:12 +0200 |
paulson |
zadd_ac and zmult_ac are no longer included by default
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:29:01 +0200 |
paulson |
removal of rewrites for Suc(Suc(Suc...)))
|
file |
diff |
annotate
|
| Thu, 15 Jul 1999 10:33:16 +0200 |
paulson |
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
|
file |
diff |
annotate
|
| Wed, 14 Jul 1999 10:39:26 +0200 |
paulson |
new constant folding rewrites
|
file |
diff |
annotate
|
| Tue, 13 Jul 1999 10:43:31 +0200 |
paulson |
new theorem zmult_eq_0_iff
|
file |
diff |
annotate
|
| Mon, 12 Jul 1999 10:32:30 +0200 |
paulson |
new theorems for the "at most" relation
|
file |
diff |
annotate
|
| Fri, 09 Jul 1999 10:45:09 +0200 |
paulson |
products of signs as equivalences
|
file |
diff |
annotate
|
| Thu, 08 Jul 1999 13:43:42 +0200 |
paulson |
Introduction of integer division algorithm
|
file |
diff |
annotate
|
| Tue, 06 Jul 1999 21:14:34 +0200 |
wenzelm |
use generic numeral encoding and syntax;
|
file |
diff |
annotate
|
| Wed, 23 Jun 1999 10:36:59 +0200 |
paulson |
rewrite rules to distribute CONSTANT multiplication over sum and difference;
|
file |
diff |
annotate
|
| Mon, 24 May 1999 15:54:12 +0200 |
paulson |
Better simplification of (nat #0), (int (Suc 0)), etc
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:53:46 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Wed, 03 Mar 1999 11:15:18 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Wed, 27 Jan 1999 17:11:39 +0100 |
nipkow |
arith_tac for min/max
|
file |
diff |
annotate
|
| Thu, 14 Jan 1999 13:18:09 +0100 |
nipkow |
More arith refinements.
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 08:41:28 +0100 |
nipkow |
Simplified arithmetic.
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 15:59:35 +0100 |
nipkow |
Restructured Arithmatic
|
file |
diff |
annotate
|
| Mon, 11 Jan 1999 16:50:49 +0100 |
nipkow |
More arith simplifications.
|
file |
diff |
annotate
|
| Sat, 09 Jan 1999 15:24:11 +0100 |
nipkow |
Refined arith tactic.
|
file |
diff |
annotate
|
| Tue, 05 Jan 1999 17:28:14 +0100 |
nipkow |
Instantiated lin.arith.
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:46:44 +0100 |
paulson |
fixed comments
|
file |
diff |
annotate
|
| Fri, 30 Oct 1998 10:43:12 +0100 |
paulson |
Explicit (and improved) simprules for binary arithmetic.
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 18:47:44 +0200 |
paulson |
Now users will never see (int 0)
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:25:18 +0200 |
paulson |
better handling of literals
|
file |
diff |
annotate
|
| Tue, 29 Sep 1998 15:57:42 +0200 |
paulson |
many renamings and changes. Simproc for cancelling common terms in relations
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 13:57:01 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 17:07:24 +0200 |
paulson |
renamed some axioms; some new theorems
|
file |
diff |
annotate
|
| Wed, 23 Sep 1998 10:25:37 +0200 |
paulson |
much renaming and reorganization
|
file |
diff |
annotate
|
| Mon, 21 Sep 1998 10:43:09 +0200 |
paulson |
much renaming and tidying
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 16:05:08 +0200 |
paulson |
improved (but still flawed) treatment of binary arithmetic
|
file |
diff |
annotate
|