| Fri, 09 Oct 1998 11:15:39 +0200 |
nipkow |
added Induct/Multiset*
|
changeset |
files
|
| Fri, 09 Oct 1998 11:15:07 +0200 |
nipkow |
New inductive definition of `card'
|
changeset |
files
|
| Fri, 09 Oct 1998 11:10:59 +0200 |
paulson |
polymorphic versions of nat_neq_iff and nat_neqE
|
changeset |
files
|
| Thu, 08 Oct 1998 11:59:17 +0200 |
nipkow |
Further improvement of the simplifier.
|
changeset |
files
|
| Wed, 07 Oct 1998 18:17:37 +0200 |
nipkow |
Tuned simplifier not to re-normalized already normalized terms.
|
changeset |
files
|
| Wed, 07 Oct 1998 17:51:11 +0200 |
wenzelm |
tuned rm CVS;
|
changeset |
files
|
| Wed, 07 Oct 1998 13:21:50 +0200 |
nipkow |
runs test
|
changeset |
files
|
| Wed, 07 Oct 1998 10:32:00 +0200 |
paulson |
tidying and renaming
|
changeset |
files
|
| Wed, 07 Oct 1998 10:31:30 +0200 |
paulson |
new theorems
|
changeset |
files
|
| Wed, 07 Oct 1998 10:31:07 +0200 |
paulson |
tidied
|
changeset |
files
|
| Wed, 07 Oct 1998 10:30:47 +0200 |
paulson |
new files UNITY/Comp.{thy,ML}
|
changeset |
files
|
| Tue, 06 Oct 1998 14:39:53 +0200 |
nipkow |
Merges FoldSet into Finite
|
changeset |
files
|
| Mon, 05 Oct 1998 10:33:34 +0200 |
paulson |
deleted incorrect code that set Goals.proof_timing:=false
|
changeset |
files
|
| Mon, 05 Oct 1998 10:31:43 +0200 |
paulson |
Now prove_goalw_cterm never prints timing statistics
|
changeset |
files
|