diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-09-28 09:03:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-09-28 09:03:56 +0000 |
| commit | 41ffd7a69ab0c181d6ad3c8866e24b4feebcde70 (patch) | |
| tree | b78c91a29c6d0e796bd35537ea5945caaa595509 /twelf/example.elf | |
| parent | cf3a7463ade0ffe5a3f20c900cad898074b1a4e4 (diff) | |
Fixes to twelf support, begins to work now.
Diffstat (limited to 'twelf/example.elf')
| -rw-r--r-- | twelf/example.elf | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/twelf/example.elf b/twelf/example.elf index e52d5a06..b4281734 100644 --- a/twelf/example.elf +++ b/twelf/example.elf @@ -4,6 +4,11 @@ %%% $Id$ %%% +%%% Rather than a proof this file is just a signature, +%%% bunch of declarations. Would be nice to have something +%%% closer to other systems for pedagogical purposes... +%%% (i.e. proving commutativity of conjunction in ND fragment +%%% of this logic) %%% Intuitionistic propositional calculus %%% Positive fragment with implies, and, true. |