| 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
|
| Tue, 15 Sep 1998 15:06:29 +0200 |
paulson |
revised treatment of integers
|
file |
diff |
annotate
|
| Fri, 31 Jul 1998 10:50:47 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 17:55:57 +0200 |
wenzelm |
added ex/MonoidGroups (record example);
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Sat, 07 Mar 1998 16:29:29 +0100 |
nipkow |
Removed `addsplits [expand_if]'
|
file |
diff |
annotate
|
| Fri, 20 Feb 1998 17:56:51 +0100 |
nipkow |
Congruence rules use == in premises now.
|
file |
diff |
annotate
|
| Mon, 10 Nov 1997 15:25:12 +0100 |
wenzelm |
ASCII-fied;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 15:25:12 +0200 |
nipkow |
setloop split_tac -> addsplits
|
file |
diff |
annotate
|
| Fri, 18 Apr 1997 11:54:54 +0200 |
paulson |
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
|
file |
diff |
annotate
|
| Tue, 26 Nov 1996 15:59:28 +0100 |
paulson |
New material from Norbert Voelker for efficient binary comparisons
|
file |
diff |
annotate
|
| Tue, 30 Jul 1996 17:33:26 +0200 |
berghofe |
Classical tactics now use default claset.
|
file |
diff |
annotate
|
| Fri, 29 Mar 1996 13:18:26 +0100 |
paulson |
Binary integers and their numeric syntax
|
file |
diff |
annotate
|