| Thu, 24 Oct 1996 10:31:17 +0200 |
paulson |
Moved ex_strip_tac to the common part
|
changeset |
files
|
| Thu, 24 Oct 1996 10:30:43 +0200 |
paulson |
Removal of unused predicate isSpy
|
changeset |
files
|
| Thu, 24 Oct 1996 10:30:17 +0200 |
paulson |
Handles pathnames in ISABELLECOMP
|
changeset |
files
|
| Mon, 21 Oct 1996 11:37:21 +0200 |
paulson |
Mentions the possibility of pathnames in ISABELLECOMP;
|
changeset |
files
|
| Mon, 21 Oct 1996 11:36:57 +0200 |
paulson |
Creates a bigger main window
|
changeset |
files
|
| Mon, 21 Oct 1996 11:18:34 +0200 |
paulson |
ISABELLECOMP may now have a leading pathname
|
changeset |
files
|
| Mon, 21 Oct 1996 09:51:18 +0200 |
nipkow |
Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
|
changeset |
files
|
| Mon, 21 Oct 1996 09:50:50 +0200 |
nipkow |
Added trans_tac (see Provers/nat_transitive.ML)
|
changeset |
files
|
| Mon, 21 Oct 1996 09:49:41 +0200 |
nipkow |
Solves simple arithmetic goals.
|
changeset |
files
|
| Fri, 18 Oct 1996 12:54:19 +0200 |
paulson |
Subst as modified by Konrad Slind
|
changeset |
files
|
| Fri, 18 Oct 1996 12:41:04 +0200 |
paulson |
Konrad Slind's TFL
|
changeset |
files
|
| Fri, 18 Oct 1996 11:43:14 +0200 |
paulson |
New version of Yahalom, as recommended on p 259 of BAN paper
|
changeset |
files
|
| Fri, 18 Oct 1996 11:42:41 +0200 |
paulson |
Addition of Reveal message
|
changeset |
files
|
| Fri, 18 Oct 1996 11:42:17 +0200 |
paulson |
Deleted obsolete rewrites (they are now in HOL/simpdata)
|
changeset |
files
|