| Thu, 21 Apr 2005 19:16:19 +0200 |
berghofe |
Adapted use command to new behaviour of Toplevel.node_trans
|
changeset |
files
|
| Thu, 21 Apr 2005 19:13:03 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
changeset |
files
|
| Thu, 21 Apr 2005 19:12:03 +0200 |
berghofe |
- Eliminated nodup_vars check.
|
changeset |
files
|
| Thu, 21 Apr 2005 19:02:54 +0200 |
berghofe |
Moved cterm_fun from Thm to Drule.
|
changeset |
files
|
| Thu, 21 Apr 2005 18:58:44 +0200 |
berghofe |
Modified variable index in proof (necessary due to changes in the kernel).
|
changeset |
files
|
| Thu, 21 Apr 2005 18:57:18 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
changeset |
files
|
| Thu, 21 Apr 2005 18:56:03 +0200 |
berghofe |
Made inst1_tac more robust against changes of variable indices.
|
changeset |
files
|
| Thu, 21 Apr 2005 17:22:23 +0200 |
nipkow |
fix
|
changeset |
files
|
| Thu, 21 Apr 2005 17:22:17 +0200 |
nipkow |
tuning locales
|
changeset |
files
|
| Thu, 21 Apr 2005 15:33:30 +0200 |
paulson |
removed tracing info
|
changeset |
files
|
| Thu, 21 Apr 2005 15:05:24 +0200 |
paulson |
added hearder lines and deleted some redundant material
|
changeset |
files
|
| Thu, 21 Apr 2005 13:15:25 +0200 |
paulson |
adding the Proof General preview
|
changeset |
files
|
| Thu, 21 Apr 2005 10:05:06 +0200 |
paulson |
improved SML/NJ compatibility, etc.
|
changeset |
files
|
| Wed, 20 Apr 2005 22:43:52 +0200 |
gagern |
Added op in front of constructor for better parsing.
|
changeset |
files
|
| Wed, 20 Apr 2005 22:37:29 +0200 |
gagern |
Fix automatic determination of poly version.
|
changeset |
files
|
| Wed, 20 Apr 2005 19:00:30 +0200 |
gagern |
removed redundant readlink call
|
changeset |
files
|
| Wed, 20 Apr 2005 18:57:05 +0200 |
webertj |
call to Array.modifyi replaced
|
changeset |
files
|
| Wed, 20 Apr 2005 18:01:50 +0200 |
quigley |
Corrected the problem with the ATP directory.
|
changeset |
files
|
| Wed, 20 Apr 2005 17:19:42 +0200 |
nipkow |
Used locale interpretations everywhere. -> lemma had new name
|
changeset |
files
|
| Wed, 20 Apr 2005 17:19:18 +0200 |
nipkow |
Used locale interpretations everywhere.
|
changeset |
files
|
| Wed, 20 Apr 2005 16:03:17 +0200 |
quigley |
Removed remaining references to Main.thy in reconstruction code.
|
changeset |
files
|
| Wed, 20 Apr 2005 14:18:33 +0200 |
gagern |
Allow symlinks to shell scripts
|
changeset |
files
|
| Wed, 20 Apr 2005 00:45:54 +0200 |
kleing |
added locale instantiation
|
changeset |
files
|
| Tue, 19 Apr 2005 18:46:04 +0200 |
webertj |
refute extended
|
changeset |
files
|
| Tue, 19 Apr 2005 18:08:55 +0200 |
paulson |
syntax fix
|
changeset |
files
|
| Tue, 19 Apr 2005 18:08:44 +0200 |
paulson |
more tidying of libraries in Reconstruction
|
changeset |
files
|
| Tue, 19 Apr 2005 15:15:06 +0200 |
quigley |
Completed integration of reconstruction code. Now finds and displays proofs when used with modified version
|
changeset |
files
|
| Tue, 19 Apr 2005 13:35:01 +0200 |
paulson |
auto update
|
changeset |
files
|