| Wed, 23 Sep 1998 10:25:37 +0200 |
paulson |
much renaming and reorganization
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 16:04:44 +0200 |
paulson |
Now defines "int" as a linear order; basic derivations moved to IntDef
|
file |
diff |
annotate
|
| Tue, 15 Sep 1998 15:06:29 +0200 |
paulson |
revised treatment of integers
|
file |
diff |
annotate
|
| Thu, 10 Sep 1998 17:26:16 +0200 |
paulson |
well-formed zless_asym; tidied
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:14:26 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 14:19:02 +0200 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:15:13 +0200 |
paulson |
Removal of leading "\!\!..." from most Goal commands
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Mon, 27 Apr 1998 16:45:27 +0200 |
nipkow |
Renamed expand_const -> split_const.
|
file |
diff |
annotate
|
| Tue, 21 Apr 1998 17:22:47 +0200 |
oheimb |
made proof of zmult_congruent2 more stable
|
file |
diff |
annotate
|
| Thu, 02 Apr 1998 17:19:02 +0200 |
oheimb |
split_all_tac now fails if there is nothing to split
|
file |
diff |
annotate
|
| Tue, 03 Mar 1998 15:15:04 +0100 |
paulson |
Better simplification allows deletion of parts of proofs
|
file |
diff |
annotate
|
| Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
| Tue, 23 Dec 1997 11:49:46 +0100 |
paulson |
Decremented subscript because of change to iffD1
|
file |
diff |
annotate
|
| Fri, 05 Dec 1997 17:14:36 +0100 |
wenzelm |
adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
|
file |
diff |
annotate
|
| Mon, 10 Nov 1997 15:25:12 +0100 |
wenzelm |
ASCII-fied;
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 13:50:59 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Mon, 29 Sep 1997 11:40:03 +0200 |
paulson |
result() -> qed
|
file |
diff |
annotate
|
| Tue, 25 Feb 1997 15:12:49 +0100 |
pusch |
minor changes due to primrec defintions for +,-,*
|
file |
diff |
annotate
|
| Fri, 07 Feb 1997 14:13:58 +0100 |
nipkow |
Modified proofs because of added "triv_forall_equality".
|
file |
diff |
annotate
|
| Tue, 26 Nov 1996 15:59:28 +0100 |
paulson |
New material from Norbert Voelker for efficient binary comparisons
|
file |
diff |
annotate
|
| Thu, 21 Nov 1996 15:28:25 +0100 |
paulson |
Tidied up some proofs, ...
|
file |
diff |
annotate
|
| Thu, 10 Oct 1996 10:47:26 +0200 |
paulson |
Tidied some proofs: changed needed for de Morgan laws
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 16:38:02 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
file |
diff |
annotate
|
| Tue, 30 Jul 1996 17:33:26 +0200 |
berghofe |
Classical tactics now use default claset.
|
file |
diff |
annotate
|
| Fri, 14 Jun 1996 12:25:02 +0200 |
paulson |
Explicitly included add_mult_distrib & add_mult_distrib2
|
file |
diff |
annotate
|
| Wed, 27 Mar 1996 18:46:42 +0100 |
paulson |
Now use _irrefl instead of _anti_refl
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:12:14 +0100 |
clasohm |
added local simpsets
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:04:45 +0100 |
clasohm |
new version of HOL/Integ with curried function application
|
file |
diff |
annotate
|