| Wed, 03 Mar 1999 11:15:18 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Tue, 19 Jan 1999 11:18:11 +0100 |
paulson |
removal of the (thm list) argument of mk_cases
|
file |
diff |
annotate
|
| Thu, 14 Jan 1999 13:18:09 +0100 |
nipkow |
More arith refinements.
|
file |
diff |
annotate
|
| Mon, 11 Jan 1999 16:50:49 +0100 |
nipkow |
More arith simplifications.
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 17:00:30 +0100 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| Fri, 09 Oct 1998 11:10:59 +0200 |
paulson |
polymorphic versions of nat_neq_iff and nat_neqE
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 10:33:54 +0200 |
nipkow |
First steps towards termination of simply typed terms.
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:19:38 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 12:02:19 +0200 |
nipkow |
@ -> $
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 10:36:47 +0200 |
nipkow |
Removed leading !! in goals.
|
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
|
| Sat, 07 Mar 1998 16:29:29 +0100 |
nipkow |
Removed `addsplits [expand_if]'
|
file |
diff |
annotate
|
| Thu, 04 Dec 1997 12:44:37 +0100 |
nipkow |
pred n -> n-1
|
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
|
| Fri, 17 Oct 1997 15:25:12 +0200 |
nipkow |
setloop split_tac -> addsplits
|
file |
diff |
annotate
|
| Mon, 21 Apr 1997 10:13:47 +0200 |
paulson |
Now faster without calling Blast.depth_tac
|
file |
diff |
annotate
|
| Thu, 10 Apr 1997 12:21:21 +0200 |
nipkow |
Mod because of "Turned Addsimps into AddIffs for datatype laws."
|
file |
diff |
annotate
|
| Wed, 09 Apr 1997 12:32:04 +0200 |
paulson |
Using Blast_tac
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 11:18:52 +0200 |
paulson |
Calls Blast_tac
|
file |
diff |
annotate
|
| Mon, 04 Nov 1996 17:23:37 +0100 |
nipkow |
Used nat_trans_tac. New Eta. various smaller changes.
|
file |
diff |
annotate
|
| Mon, 21 Oct 1996 09:51:18 +0200 |
nipkow |
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
|
file |
diff |
annotate
|
| Thu, 10 Oct 1996 10:47:26 +0200 |
paulson |
Tidied some proofs: changed needed for de Morgan laws
|
file |
diff |
annotate
|
| Mon, 07 Oct 1996 10:31:50 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Wed, 11 Sep 1996 15:17:07 +0200 |
nipkow |
Removed refs to clasets like rel_cs etc. Used implicit claset.
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:17:20 +0200 |
paulson |
Tidied some proofs, maybe using less_SucE
|
file |
diff |
annotate
|
| Wed, 22 May 1996 18:32:37 +0200 |
nipkow |
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
|
file |
diff |
annotate
|
| Tue, 07 May 1996 18:19:13 +0200 |
paulson |
Updated for new form of induction rules
|
file |
diff |
annotate
|
| Tue, 23 Apr 1996 16:58:57 +0200 |
oheimb |
repaired critical proofs depending on the order inside non-confluent SimpSets
|
file |
diff |
annotate
|
| Fri, 09 Feb 1996 13:41:59 +0100 |
nipkow |
Introduced qed_spec_mp.
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Tue, 02 Jan 1996 14:08:04 +0100 |
nipkow |
Polished proofs.
|
file |
diff |
annotate
|
| Wed, 25 Oct 1995 09:49:35 +0100 |
nipkow |
Moved some thms to Arith and to Trancl.
|
file |
diff |
annotate
|
| Fri, 06 Oct 1995 10:45:11 +0100 |
nipkow |
New version with eta reduction.
|
file |
diff |
annotate
|