| Wed, 18 Aug 1999 18:44:20 +0200 |
paulson |
from Konrad: support for schematic definitions
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 17:43:53 +0200 |
berghofe |
Removed rbeta.
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 12:23:10 +0200 |
paulson |
new version from Konrad with "lazy" (deferred) definitons
|
file |
diff |
annotate
|
| Fri, 23 Apr 1999 12:23:21 +0200 |
paulson |
Now for recdefs that omit the WF relation;
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:27:28 +0200 |
paulson |
Numerous simplifications and removal of HOL-isms
|
file |
diff |
annotate
|
| Fri, 30 May 1997 15:55:27 +0200 |
paulson |
Simplified the calling sequence of CONTEXT_REWRITE_RULE
|
file |
diff |
annotate
|
| Tue, 27 May 1997 13:22:30 +0200 |
paulson |
Removal of module Mask and datatype binding with its constructor |->
|
file |
diff |
annotate
|
| Thu, 22 May 1997 15:13:16 +0200 |
paulson |
New headers and other minor changes
|
file |
diff |
annotate
|
| Tue, 20 May 1997 11:49:57 +0200 |
paulson |
Removal of redundant code (unused or already present in Isabelle.
|
file |
diff |
annotate
|
| Fri, 18 Oct 1996 12:41:04 +0200 |
paulson |
Konrad Slind's TFL
|
file |
diff |
annotate
|