From 41ffd7a69ab0c181d6ad3c8866e24b4feebcde70 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 28 Sep 2000 09:03:56 +0000 Subject: Fixes to twelf support, begins to work now. --- twelf/example.elf | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'twelf/example.elf') 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. -- cgit v1.2.3