10 files changed, 44 insertions, 837 deletions

diff --git a/lang/twelf/Makefile b/lang/twelf/Makefile
index 78fd521463e7..cb6b20cd0587 100644
--- a/lang/twelf/Makefile
+++ b/lang/twelf/Makefile
@@ -2,41 +2,59 @@
 # $FreeBSD$
 
 PORTNAME=	twelf
-PORTVERSION=	1.5R1
-PORTREVISION=	5
-CATEGORIES=	lang
-MASTER_SITES=	http://www-2.cs.cmu.edu/~twelf/dist/ http://www.cs.cmu.edu/~twelf/dist/
-DISTNAME=	twelf-1-5R1
+PORTVERSION=	1.7.1
+CATEGORIES=	lang math
+MASTER_SITES=	http://twelf.plparty.org/releases/ \
+	http://www-2.cs.cmu.edu/~twelf/dist/ http://www.cs.cmu.edu/~twelf/dist/
+DISTNAME=	${PORTNAME}-src-${PORTVERSION}
 
-MAINTAINER=	ports@FreeBSD.org
+MAINTAINER=	beyert@cs.ucr.edu
 COMMENT=	Meta-logical framework for deductive systems
 
-.if defined(WITH_MLTON)
+LICENSE=	BSD2CLAUSE
+LICENSE_FILE=	${WRKSRC}/LICENSE
+
 RUN_DEPENDS=	mlton:${PORTSDIR}/lang/mlton
 BUILD_DEPENDS=	mlton:${PORTSDIR}/lang/mlton
-.elif defined(WITH_SML_NJ_DEVEL)
-RUN_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj-devel
-BUILD_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj-devel
-.else
-RUN_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj
-BUILD_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj
-.endif
 
+USES=	gmake
+ALL_TARGET=	mlton
+PLIST_FILES=	bin/${PORTNAME}-server
+PORTDATA=	emacs examples examples-clp examples-delphin tex vim README
+PORTDOCS=	dvi html info pdf ps
+
+.include <bsd.port.options.mk>
+
+.if ${PORT_OPTIONS:MDOCS}
 USE_TEX=	tex:build
+BUILD_DEPENDS+=	${LOCALBASE}/bin/makeinfo:${PORTSDIR}/print/texinfo
+BUILD_DEPENDS+=	${LOCALBASE}/bin/dvips:${PORTSDIR}/print/dvipsk-tetex
+.endif
 
-.if defined(WITH_MLTON)
-MAKEFILE=	mlton/Makefile
-.elif defined(WITH_SML_NJ_DEVEL)
-MAKEFILE=	smlnj/Makefile
+post-patch:
+.if ${PORT_OPTIONS:MDOCS}
+	@${REINPLACE_CMD} 's|-number|-number-sections|g' \
+		${WRKSRC}/doc/guide/Makefile
+	@${REINPLACE_CMD} 's|twelf_\*.html|twelf/\*.html|g' \
+		${WRKSRC}/doc/guide/Makefile
 .endif
 
-WRKSRC=		${WRKDIR}/twelf
-INFO=		twelf
+post-build:
+.if ${PORT_OPTIONS:MDOCS}
+	cd ${WRKSRC}/doc/guide && ${MAKE} all ${INSTALL_TARGET}
+.endif
 
-RESTRICTED=	License is currently indeterminate (expected to be GPL)
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/bin/${PORTNAME}-server \
+		${STAGEDIR}${PREFIX}/bin
+	${MKDIR} ${STAGEDIR}${DATADIR}
+	cd ${WRKSRC} && ${COPYTREE_SHARE} "${PORTDATA}" ${STAGEDIR}${DATADIR}
+.if ${PORT_OPTIONS:MDOCS}
+	@${MKDIR} ${STAGEDIR}${DOCSDIR}
+	cd ${WRKSRC}/doc && ${COPYTREE_SHARE} "${PORTDOCS}" ${STAGEDIR}${DOCSDIR}
+.endif
 
-NO_STAGE=	yes
-post-patch:
-	@${REINPLACE_CMD} -e "s|%%PREFIX%%|${PREFIX}|g" ${WRKSRC}/Makefile
+WRKSRC=		${WRKDIR}/twelf
+INFO=		twelf
 
 .include <bsd.port.mk>
diff --git a/lang/twelf/distinfo b/lang/twelf/distinfo
index 7db8dbbd5d47..2ad884334bc7 100644
--- a/lang/twelf/distinfo
+++ b/lang/twelf/distinfo
@@ -1,2 +1,2 @@
-SHA256 (twelf-1-5R1.tar.gz) = d20473493cd39e111ce3585f8c32eefc79de4099ae4e97bfe2eb7695d6987564
-SIZE (twelf-1-5R1.tar.gz) = 1157430
+SHA256 (twelf-src-1.7.1.tar.gz) = 91b0d4d8c2e54452a042da0ff642f3b46b25efb36a84497aa8b96598f49a213a
+SIZE (twelf-src-1.7.1.tar.gz) = 1147610
diff --git a/lang/twelf/files/patch-FreeBSD.mk b/lang/twelf/files/patch-FreeBSD.mk
deleted file mode 100644
index 1522b132bed8..000000000000
--- a/lang/twelf/files/patch-FreeBSD.mk
+++ /dev/null
@@ -1,170 +0,0 @@
---- FreeBSD.mk.orig	2009-02-12 21:33:04.000000000 -0500
-+++ FreeBSD.mk	2009-02-12 21:48:54.000000000 -0500
-@@ -0,0 +1,82 @@
-+# ---------------------------------------------------------------
-+# Executables
-+# ---------------------------------------------------------------
-+
-+arch != uname -p
-+
-+.if ${arch} == "i386"
-+smlarch = x86
-+.else
-+smlarch = ${arch}
-+.endif
-+
-+prefix        = ${PREFIX}
-+bindir        = ${prefix}/bin
-+infodir       = ${prefix}/info
-+twelfexecdir  = ${prefix}/libexec/twelf
-+twelfsharedir = ${prefix}/share/twelf
-+
-+runfile  = bin/twelf-server
-+heapfile = bin/.heap/twelf-server.${smlarch}-bsd
-+
-+# ---------------------------------------------------------------
-+# Documentation
-+# ---------------------------------------------------------------
-+
-+htmlnodes = toc abt 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
-+
-+dvifile = doc/dvi/twelf.dvi
-+htmlfiles := doc/html/index.html ${htmlnodes:%=doc/html/twelf_%.html}
-+infofile = doc/info/twelf.info
-+pdffile = doc/pdf/twelf.pdf
-+psfile = doc/ps/twelf.ps
-+
-+docfiles = ${dvifile} ${htmlfiles} ${infofile} ${pdffile} ${psfile}
-+
-+.for file in ${docfiles}
-+${file}:
-+	(cd doc/guide; make; make install)
-+.endfor
-+
-+all: ${runfile} ${heapfile} ${docfiles}
-+
-+# ---------------------------------------------------------------
-+# Installation
-+# ---------------------------------------------------------------
-+
-+sharefiles != (echo README HISTORY;                            \
-+               echo ${docfiles};                               \
-+               find emacs        -type f -not -path '*/CVS/*'; \
-+               find examples     -type f -not -path '*/CVS/*'; \
-+               find examples-clp -type f -not -path '*/CVS/*'; \
-+               find exercises    -type f -not -path '*/CVS/*'; \
-+               find tex          -type f -not -path '*/CVS/*'; \
-+               find vim          -type f -not -path '*/CVS/*' )
-+
-+installfiles := ${bindir}/twelf-server             \
-+                ${twelfsharedir}/${runfile}        \
-+                ${twelfexecdir}/${heapfile}        \
-+                ${infodir}/twelf.info              \
-+                ${sharefiles:%=$(twelfsharedir)/%}
-+
-+${bindir}/twelf-server: ${twelfsharedir}/${runfile}
-+	ln -s $? $@
-+
-+${twelfsharedir}/${runfile}: ${runfile}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0555 $? $@
-+
-+${twelfexecdir}/${heapfile}: ${heapfile}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0444 $? $@
-+
-+${infodir}/twelf.info: doc/info/twelf.info
-+	install -o root -g wheel -m 0444 $? $@
-+
-+.for file in ${sharefiles}
-+${twelfsharedir}/${file}: ${file}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0644 $? $@
-+.endfor
-+
-+install: ${installfiles}
---- FreeBSD.mk.orig	2009-02-12 21:33:04.000000000 -0500
-+++ FreeBSD.mk	2009-02-12 21:48:54.000000000 -0500
-@@ -0,0 +1,82 @@
-+# ---------------------------------------------------------------
-+# Executables
-+# ---------------------------------------------------------------
-+
-+arch != uname -p
-+
-+.if ${arch} == "i386"
-+smlarch = x86
-+.else
-+smlarch = ${arch}
-+.endif
-+
-+prefix        = ${PREFIX}
-+bindir        = ${prefix}/bin
-+infodir       = ${prefix}/info
-+twelfexecdir  = ${prefix}/libexec/twelf
-+twelfsharedir = ${prefix}/share/twelf
-+
-+runfile  = bin/twelf-server
-+heapfile = bin/.heap/twelf-server.${smlarch}-bsd
-+
-+# ---------------------------------------------------------------
-+# Documentation
-+# ---------------------------------------------------------------
-+
-+htmlnodes = toc abt 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
-+
-+dvifile = doc/dvi/twelf.dvi
-+htmlfiles := doc/html/index.html ${htmlnodes:%=doc/html/twelf_%.html}
-+infofile = doc/info/twelf.info
-+pdffile = doc/pdf/twelf.pdf
-+psfile = doc/ps/twelf.ps
-+
-+docfiles = ${dvifile} ${htmlfiles} ${infofile} ${pdffile} ${psfile}
-+
-+.for file in ${docfiles}
-+${file}:
-+	(cd doc/guide; make; make install)
-+.endfor
-+
-+all: ${runfile} ${heapfile} ${docfiles}
-+
-+# ---------------------------------------------------------------
-+# Installation
-+# ---------------------------------------------------------------
-+
-+sharefiles != (echo README HISTORY;                            \
-+               echo ${docfiles};                               \
-+               find emacs        -type f -not -path '*/CVS/*'; \
-+               find examples     -type f -not -path '*/CVS/*'; \
-+               find examples-clp -type f -not -path '*/CVS/*'; \
-+               find exercises    -type f -not -path '*/CVS/*'; \
-+               find tex          -type f -not -path '*/CVS/*'; \
-+               find vim          -type f -not -path '*/CVS/*' )
-+
-+installfiles := ${bindir}/twelf-server             \
-+                ${twelfsharedir}/${runfile}        \
-+                ${twelfexecdir}/${heapfile}        \
-+                ${infodir}/twelf.info              \
-+                ${sharefiles:%=$(twelfsharedir)/%}
-+
-+${bindir}/twelf-server: ${twelfsharedir}/${runfile}
-+	ln -s $? $@
-+
-+${twelfsharedir}/${runfile}: ${runfile}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0555 $? $@
-+
-+${twelfexecdir}/${heapfile}: ${heapfile}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0444 $? $@
-+
-+${infodir}/twelf.info: doc/info/twelf.info
-+	install -o root -g wheel -m 0444 $? $@
-+
-+.for file in ${sharefiles}
-+${twelfsharedir}/${file}: ${file}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0644 $? $@
-+.endfor
-+
-+install: ${installfiles}
diff --git a/lang/twelf/files/patch-Makefile b/lang/twelf/files/patch-Makefile
deleted file mode 100644
index 992543b181ec..000000000000
--- a/lang/twelf/files/patch-Makefile
+++ /dev/null
@@ -1,26 +0,0 @@
---- Makefile.orig	2005-03-08 15:49:53.000000000 -0500
-+++ Makefile	2009-02-12 22:07:33.000000000 -0500
-@@ -32,16 +32,20 @@
- version = "1.5"
- delphinversion = "0.1"
- 
-+.include "FreeBSD.mk"
-+
- default : twelf-server twelf-emacs
- 
--all : twelf-server twelf-sml twelf-emacs
-+#all : twelf-server twelf-sml twelf-emacs
- 
--twelf-server: ; 
-+${runfile}: ;
- 	@echo "*************************************************"
- 	@echo "Twelf $(version): Server"
- 	@echo "*************************************************"	 
- 	$(sml) < twelf-server.sml ;
--	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" ;
-+	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" "$(twelfexecdir)" ;
-+
-+${heapfile}: ${runfile}
- 
- twelf-sml: ; 
- 	@echo "*************************************************"
diff --git a/lang/twelf/files/patch-bin-mkexec b/lang/twelf/files/patch-bin-mkexec
deleted file mode 100644
index 216c90f8d557..000000000000
--- a/lang/twelf/files/patch-bin-mkexec
+++ /dev/null
@@ -1,13 +0,0 @@
---- bin/.mkexec.orig	2003-01-21 01:03:32.000000000 -0500
-+++ bin/.mkexec	2009-02-12 21:24:27.000000000 -0500
-@@ -7,8 +7,9 @@
- # $2 = Twelf root directory
- # $3 = Type of executable (e.g. twelf-server, twelf-sml)
- # $4 = Name of executable (e.g. twelf-server, twelf-sml)
-+# $5 = Twelf installation directory (e.g. /usr/local/libexec/twelf)
- cat > "$2/bin/$4" <<EOF
- #! /bin/sh
--exec "$1" @SMLload="$2/bin/.heap/$3" @SMLdebug=/dev/null
-+exec "$1" @SMLload="$5/bin/.heap/$3" @SMLdebug=/dev/null
- EOF
- chmod a+x "$2/bin/$4"
diff --git a/lang/twelf/files/patch-doc-guide-Makefile b/lang/twelf/files/patch-doc-guide-Makefile
deleted file mode 100644
index 74b33913e7e4..000000000000
--- a/lang/twelf/files/patch-doc-guide-Makefile
+++ /dev/null
@@ -1,11 +0,0 @@
---- doc/guide/Makefile.orig	2009-02-08 13:47:36.000000000 -0500
-+++ doc/guide/Makefile	2009-02-08 13:23:38.000000000 -0500
-@@ -39,7 +39,7 @@
- twelf_toc.html : twelf.texi;
- 	@echo "---------- Creating HTML: twelf_*.html"
- 	$(texi2html) -menu -number -split_chapter twelf.texi;
--	$(texi2html) -check *.html;
-+#	$(texi2html) -check *.html;
- 
- twelf.pdf : twelf.texi;
- 	@echo "---------- Creating unindexed PDF: twelf.pdf"
diff --git a/lang/twelf/files/patch-doc-guide-twelf.texi b/lang/twelf/files/patch-doc-guide-twelf.texi
deleted file mode 100644
index 0d1ded32f9ba..000000000000
--- a/lang/twelf/files/patch-doc-guide-twelf.texi
+++ /dev/null
@@ -1,14 +0,0 @@
---- doc/guide/twelf.texi.orig	2009-02-08 18:21:50.000000000 -0500
-+++ doc/guide/twelf.texi	2009-02-08 18:23:11.000000000 -0500
-@@ -12,6 +12,11 @@
- @syncodeindex fn cp
- @c %**end of header
- 
-+@dircategory Programming
-+@direntry
-+* Twelf User Guide: (twelf).   The Twelf User's Guide.
-+@end direntry
-+
- @titlepage
- @title Twelf User's Guide
- @subtitle Version @value{VERSION}
diff --git a/lang/twelf/files/patch-mlton-Makefile b/lang/twelf/files/patch-mlton-Makefile
deleted file mode 100644
index 9b13fcb758f2..000000000000
--- a/lang/twelf/files/patch-mlton-Makefile
+++ /dev/null
@@ -1,30 +0,0 @@
---- mlton/Makefile.orig	2004-11-12 14:10:27.000000000 -0500
-+++ mlton/Makefile	2009-02-12 22:40:25.000000000 -0500
-@@ -28,11 +28,13 @@
- version = "1.5"
- delphinversion = "0.1"
- 
-+.include "FreeBSD.mk"
-+
- default : twelf-server twelf-emacs
- 
--all : twelf-server twelf-emacs
-+#all : twelf-server twelf-emacs
- 
--twelf-server: ; 
-+${runfile}: ; 
- 	@echo "*************************************************"
- 	@echo "Twelf $(version): Server"
- 	@echo "*************************************************"
-@@ -47,7 +49,10 @@
- 		cmfileid="-97";						\
- 	fi;								\
- 	$(sml) mlton/twelf-server$${cmfileid}.cm ;			\
--	mv mlton/twelf-server$${cmfileid} bin/$(twelfserver)
-+	mv mlton/twelf-server$${cmfileid} ${runfile}
-+
-+${heapfile}:
-+	touch ${heapfile}
- 
- twelf-sml: ; 
- 	@echo "*************************************************"
diff --git a/lang/twelf/files/patch-smlnj-Makefile b/lang/twelf/files/patch-smlnj-Makefile
deleted file mode 100644
index 739869e21e6f..000000000000
--- a/lang/twelf/files/patch-smlnj-Makefile
+++ /dev/null
@@ -1,26 +0,0 @@
---- smlnj/Makefile.orig	2003-10-17 23:35:23.000000000 -0400
-+++ smlnj/Makefile	2009-02-12 22:22:57.000000000 -0500
-@@ -32,16 +32,20 @@
- version = "1.5"
- delphinversion = "0.1"
- 
-+.include "FreeBSD.mk"
-+
- default : twelf-server twelf-emacs
- 
--all : twelf-server twelf-sml twelf-emacs
-+#all : twelf-server twelf-sml twelf-emacs
- 
--twelf-server: ; 
-+${runfile}: ; 
- 	@echo "*************************************************"
- 	@echo "Twelf $(version): Server"
- 	@echo "*************************************************"	 
- 	$(sml) < smlnj/twelf-server.sml ;
--	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" ;
-+	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" "$(twelfexecdir)" ;
-+
-+${heapfile}: ${runfile}
- 
- twelf-sml: ; 
- 	@echo "*************************************************"
diff --git a/lang/twelf/pkg-plist b/lang/twelf/pkg-plist
deleted file mode 100644
index 62958d4c8ac3..000000000000
--- a/lang/twelf/pkg-plist
+++ /dev/null
@@ -1,521 +0,0 @@
-bin/twelf-server
-libexec/twelf/bin/.heap/twelf-server.x86-bsd
-share/twelf/bin/twelf-server
-share/twelf/README
-share/twelf/HISTORY
-share/twelf/doc/dvi/twelf.dvi
-share/twelf/doc/html/index.html
-share/twelf/doc/html/twelf_toc.html
-share/twelf/doc/html/twelf_abt.html
-share/twelf/doc/html/twelf_1.html
-share/twelf/doc/html/twelf_2.html
-share/twelf/doc/html/twelf_3.html
-share/twelf/doc/html/twelf_4.html
-share/twelf/doc/html/twelf_5.html
-share/twelf/doc/html/twelf_6.html
-share/twelf/doc/html/twelf_7.html
-share/twelf/doc/html/twelf_8.html
-share/twelf/doc/html/twelf_9.html
-share/twelf/doc/html/twelf_10.html
-share/twelf/doc/html/twelf_11.html
-share/twelf/doc/html/twelf_12.html
-share/twelf/doc/html/twelf_13.html
-share/twelf/doc/html/twelf_14.html
-share/twelf/doc/html/twelf_15.html
-share/twelf/doc/html/twelf_16.html
-share/twelf/doc/html/twelf_17.html
-share/twelf/doc/html/twelf_18.html
-share/twelf/doc/html/twelf_19.html
-share/twelf/doc/html/twelf_20.html
-share/twelf/doc/info/twelf.info
-share/twelf/doc/pdf/twelf.pdf
-share/twelf/doc/ps/twelf.ps
-share/twelf/emacs/.cvsignore
-share/twelf/emacs/README
-share/twelf/emacs/auc-menu.el
-share/twelf/emacs/twelf-font.el
-share/twelf/emacs/twelf-hilit.el
-share/twelf/emacs/twelf-init.el
-share/twelf/emacs/twelf.el
-share/twelf/examples/arith/arith.elf
-share/twelf/examples/arith/README
-share/twelf/examples/arith/arith.thm
-share/twelf/examples/arith/sources.cfg
-share/twelf/examples/arith/test.cfg
-share/twelf/examples/README
-share/twelf/examples/ccc/abs-env.elf
-share/twelf/examples/ccc/README
-share/twelf/examples/ccc/catlem.elf
-share/twelf/examples/ccc/ccc.elf
-share/twelf/examples/ccc/conc.elf
-share/twelf/examples/ccc/conc.thm
-share/twelf/examples/ccc/cong.elf
-share/twelf/examples/ccc/eqpres1.elf
-share/twelf/examples/ccc/eqpres2.elf
-share/twelf/examples/ccc/examples.quy
-share/twelf/examples/ccc/inv1.elf
-share/twelf/examples/ccc/inv2.elf
-share/twelf/examples/ccc/lambda.elf
-share/twelf/examples/ccc/pf.dvi
-share/twelf/examples/ccc/refl.elf
-share/twelf/examples/ccc/sources.cfg
-share/twelf/examples/ccc/spass.cfg
-share/twelf/examples/ccc/spass.elf
-share/twelf/examples/ccc/spass.sml
-share/twelf/examples/ccc/subext.elf
-share/twelf/examples/ccc/test.cfg
-share/twelf/examples/church-rosser/equiv.elf
-share/twelf/examples/church-rosser/README
-share/twelf/examples/church-rosser/cr.thm
-share/twelf/examples/church-rosser/church-rosser.thm
-share/twelf/examples/church-rosser/examples.quy
-share/twelf/examples/church-rosser/lam.elf
-share/twelf/examples/church-rosser/ord-cr.elf
-share/twelf/examples/church-rosser/ord-lemmas.elf
-share/twelf/examples/church-rosser/ord-red.elf
-share/twelf/examples/church-rosser/par-cr.elf
-share/twelf/examples/church-rosser/par-lemmas.elf
-share/twelf/examples/church-rosser/par-red.elf
-share/twelf/examples/church-rosser/sources.cfg
-share/twelf/examples/church-rosser/test-unsafe.cfg
-share/twelf/examples/church-rosser/test.cfg
-share/twelf/examples/church-rosser/test.tag
-share/twelf/examples/compile/cls/cls-complete.elf
-share/twelf/examples/compile/cls/cls-sound.elf
-share/twelf/examples/compile/cls/cls.elf
-share/twelf/examples/compile/cls/compute.elf
-share/twelf/examples/compile/cls/debruijn.elf
-share/twelf/examples/compile/cls/examples.quy
-share/twelf/examples/compile/cls/feval.elf
-share/twelf/examples/compile/cls/mini-ml.elf
-share/twelf/examples/compile/cls/slow.quy
-share/twelf/examples/compile/cls/sources.cfg
-share/twelf/examples/compile/cls/test.cfg
-share/twelf/examples/compile/cls/trans.elf
-share/twelf/examples/compile/cls/trans2.elf
-share/twelf/examples/compile/README
-share/twelf/examples/compile/cpm/ceval-complete.elf
-share/twelf/examples/compile/cpm/ceval-complete.thm
-share/twelf/examples/compile/cpm/ceval-sound.elf
-share/twelf/examples/compile/cpm/ceval.elf
-share/twelf/examples/compile/cpm/cpm.elf
-share/twelf/examples/compile/cpm/evalv.elf
-share/twelf/examples/compile/cpm/examples.quy
-share/twelf/examples/compile/cpm/mini-mlv.elf
-share/twelf/examples/compile/cpm/proof-equiv.elf
-share/twelf/examples/compile/cpm/proof-equiv.thm
-share/twelf/examples/compile/cpm/slow.quy
-share/twelf/examples/compile/cpm/sources.cfg
-share/twelf/examples/compile/cpm/test.cfg
-share/twelf/examples/compile/cpm/theorems.elf
-share/twelf/examples/compile/cpm/theorems.thm
-share/twelf/examples/compile/cps/cps-eval.elf
-share/twelf/examples/compile/cps/cps.elf
-share/twelf/examples/compile/cps/examples.quy
-share/twelf/examples/compile/cps/mini-ml.elf
-share/twelf/examples/compile/cps/ml-cps.elf
-share/twelf/examples/compile/cps/sources.cfg
-share/twelf/examples/compile/cps/test.cfg
-share/twelf/examples/compile/cxm/evalv.elf
-share/twelf/examples/compile/cxm/examples.quy
-share/twelf/examples/compile/cxm/mini-mlv.elf
-share/twelf/examples/compile/cxm/sources.cfg
-share/twelf/examples/compile/cxm/test.cfg
-share/twelf/examples/compile/cxm/xeval.elf
-share/twelf/examples/compile/debruijn/debruijn.elf
-share/twelf/examples/compile/debruijn/eval.elf
-share/twelf/examples/compile/debruijn/examples.quy
-share/twelf/examples/compile/debruijn/feval.elf
-share/twelf/examples/compile/debruijn/map-eval.elf
-share/twelf/examples/compile/debruijn/mini-ml.elf
-share/twelf/examples/compile/debruijn/sources.cfg
-share/twelf/examples/compile/debruijn/test.cfg
-share/twelf/examples/compile/debruijn/trans.elf
-share/twelf/examples/compile/debruijn/val-lemmas.elf
-share/twelf/examples/compile/debruijn/value.elf
-share/twelf/examples/compile/debruijn1/debruijn.elf
-share/twelf/examples/compile/debruijn1/eval.elf
-share/twelf/examples/compile/debruijn1/examples.quy
-share/twelf/examples/compile/debruijn1/feval.elf
-share/twelf/examples/compile/debruijn1/map-eval.elf
-share/twelf/examples/compile/debruijn1/mini-ml.elf
-share/twelf/examples/compile/debruijn1/sources.cfg
-share/twelf/examples/compile/debruijn1/test.cfg
-share/twelf/examples/compile/debruijn1/trans.elf
-share/twelf/examples/cpsocc/corr.elf
-share/twelf/examples/cpsocc/NOTES
-share/twelf/examples/cpsocc/READ.ME
-share/twelf/examples/cpsocc/cpsBNF.elf
-share/twelf/examples/cpsocc/def1+5+fig4.elf
-share/twelf/examples/cpsocc/def13.elf
-share/twelf/examples/cpsocc/def16.elf
-share/twelf/examples/cpsocc/def3+6+fig5.elf
-share/twelf/examples/cpsocc/dsBNF.elf
-share/twelf/examples/cpsocc/examples.quy
-share/twelf/examples/cpsocc/examples.quy.orig
-share/twelf/examples/cpsocc/fig1.elf
-share/twelf/examples/cpsocc/fig10.elf
-share/twelf/examples/cpsocc/fig11.elf
-share/twelf/examples/cpsocc/fig12.elf
-share/twelf/examples/cpsocc/fig13.elf
-share/twelf/examples/cpsocc/fig7.elf
-share/twelf/examples/cpsocc/fig8.elf
-share/twelf/examples/cpsocc/fig9.elf
-share/twelf/examples/cpsocc/lemma14.elf
-share/twelf/examples/cpsocc/lemma17.elf
-share/twelf/examples/cpsocc/lemma7.elf
-share/twelf/examples/cpsocc/lemma9.elf
-share/twelf/examples/cpsocc/th2.elf
-share/twelf/examples/cpsocc/load.sml
-share/twelf/examples/cpsocc/sources.cfg
-share/twelf/examples/cpsocc/test.cfg
-share/twelf/examples/cpsocc/test.quy
-share/twelf/examples/cpsocc/test.quy.orig
-share/twelf/examples/cpsocc/th10.elf
-share/twelf/examples/cpsocc/th15.elf
-share/twelf/examples/cpsocc/th18.elf
-share/twelf/examples/cpsocc/th4.elf
-share/twelf/examples/cpsocc/th8.elf
-share/twelf/examples/cut-elim/cl-admit.elf
-share/twelf/examples/cut-elim/README
-share/twelf/examples/cut-elim/cl-cut.elf
-share/twelf/examples/cut-elim/cl-elim.elf
-share/twelf/examples/cut-elim/cl.elf
-share/twelf/examples/cut-elim/cl.thm
-share/twelf/examples/cut-elim/examples.quy
-share/twelf/examples/cut-elim/formulas.elf
-share/twelf/examples/cut-elim/int-admit.elf
-share/twelf/examples/cut-elim/int-cut.elf
-share/twelf/examples/cut-elim/int-elim.elf
-share/twelf/examples/cut-elim/int.elf
-share/twelf/examples/cut-elim/int.thm
-share/twelf/examples/cut-elim/sources.cfg
-share/twelf/examples/cut-elim/test.cfg
-share/twelf/examples/fol/sources.cfg
-share/twelf/examples/fol/README
-share/twelf/examples/fol/fol.elf
-share/twelf/examples/fol/fol.thm
-share/twelf/examples/fol/test.cfg
-share/twelf/examples/guide/arith.elf
-share/twelf/examples/guide/lam.elf
-share/twelf/examples/guide/lists.elf
-share/twelf/examples/guide/nd.elf
-share/twelf/examples/guide/sources.cfg
-share/twelf/examples/guide/test.cfg
-share/twelf/examples/handbook/sources.cfg
-share/twelf/examples/handbook/README
-share/twelf/examples/handbook/fol.elf
-share/twelf/examples/handbook/test.cfg
-share/twelf/examples/incll/incll.elf
-share/twelf/examples/incll/README
-share/twelf/examples/incll/bff-incll.elf
-share/twelf/examples/incll/bff-incll.quy
-share/twelf/examples/incll/cpm-incll.elf
-share/twelf/examples/incll/cpm-incll.quy
-share/twelf/examples/incll/iosequents.elf
-share/twelf/examples/incll/lists-incll.elf
-share/twelf/examples/incll/lists-incll.quy
-share/twelf/examples/incll/lists.elf
-share/twelf/examples/incll/parse-incll.elf
-share/twelf/examples/incll/parse-incll.quy
-share/twelf/examples/incll/parse-lolli.elf
-share/twelf/examples/incll/parse-lolli.quy
-share/twelf/examples/incll/pre-incll.elf
-share/twelf/examples/incll/pre-incll.quy
-share/twelf/examples/incll/search-incll.elf
-share/twelf/examples/incll/search-incll.quy
-share/twelf/examples/incll/sort-incll.elf
-share/twelf/examples/incll/sort-incll.quy
-share/twelf/examples/incll/sources.cfg
-share/twelf/examples/incll/test.cfg
-share/twelf/examples/kolm/complete.elf
-share/twelf/examples/kolm/README
-share/twelf/examples/kolm/examples.quy
-share/twelf/examples/kolm/fol.elf
-share/twelf/examples/kolm/kolmtrans.elf
-share/twelf/examples/kolm/nj.elf
-share/twelf/examples/kolm/nk.elf
-share/twelf/examples/kolm/report.ps
-share/twelf/examples/kolm/sound.elf
-share/twelf/examples/kolm/sources.cfg
-share/twelf/examples/kolm/test.cfg
-share/twelf/examples/lp/canon.elf
-share/twelf/examples/lp/cont.elf
-share/twelf/examples/lp/conv.elf
-share/twelf/examples/lp/examples.elf
-share/twelf/examples/lp/examples.quy
-share/twelf/examples/lp/fohh-formulas.elf
-share/twelf/examples/lp/fohh.elf
-share/twelf/examples/lp/iscan.elf
-share/twelf/examples/lp/natded.elf
-share/twelf/examples/lp/res-complete.elf
-share/twelf/examples/lp/res-sound.elf
-share/twelf/examples/lp/resolution.elf
-share/twelf/examples/lp/sources.cfg
-share/twelf/examples/lp/test.cfg
-share/twelf/examples/lp/uni-complete.elf
-share/twelf/examples/lp/uni-sound.elf
-share/twelf/examples/lp/uniform.elf
-share/twelf/examples/lp-horn/canon.elf
-share/twelf/examples/lp-horn/conv.elf
-share/twelf/examples/lp-horn/examples.quy
-share/twelf/examples/lp-horn/iscan.elf
-share/twelf/examples/lp-horn/natded.elf
-share/twelf/examples/lp-horn/sources.cfg
-share/twelf/examples/lp-horn/test.cfg
-share/twelf/examples/lp-horn/uni-can.elf
-share/twelf/examples/lp-horn/uni-can.thm
-share/twelf/examples/lp-horn/uni-complete.elf
-share/twelf/examples/lp-horn/uni-complete.thm
-share/twelf/examples/lp-horn/uni-sound.elf
-share/twelf/examples/lp-horn/uni-sound.thm
-share/twelf/examples/lp-horn/uniform.elf
-share/twelf/examples/mini-ml/closed.elf
-share/twelf/examples/mini-ml/README
-share/twelf/examples/mini-ml/eval.elf
-share/twelf/examples/mini-ml/eval1.elf
-share/twelf/examples/mini-ml/eval2.elf
-share/twelf/examples/mini-ml/examples.quy
-share/twelf/examples/mini-ml/examples1.quy
-share/twelf/examples/mini-ml/mini-ml.elf
-share/twelf/examples/mini-ml/reduce.elf
-share/twelf/examples/mini-ml/reduce.thm
-share/twelf/examples/mini-ml/sources.cfg
-share/twelf/examples/mini-ml/sources1.cfg
-share/twelf/examples/mini-ml/test.cfg
-share/twelf/examples/mini-ml/tp-preserve.elf
-share/twelf/examples/mini-ml/tp-preserve.thm
-share/twelf/examples/mini-ml/tp.elf
-share/twelf/examples/mini-ml/tpinf.elf
-share/twelf/examples/mini-ml/val-sound.elf
-share/twelf/examples/mini-ml/val-sound.thm
-share/twelf/examples/mini-ml/value.elf
-share/twelf/examples/polylam/examples.quy
-share/twelf/examples/polylam/polylam.elf
-share/twelf/examples/polylam/sources.cfg
-share/twelf/examples/polylam/test.cfg
-share/twelf/examples/prop-calc/equiv.elf
-share/twelf/examples/prop-calc/README
-share/twelf/examples/prop-calc/equiv.thm
-share/twelf/examples/prop-calc/examples.quy
-share/twelf/examples/prop-calc/nd.elf
-share/twelf/examples/prop-calc/nd.tex
-share/twelf/examples/prop-calc/ndclass.elf
-share/twelf/examples/prop-calc/prop-calc-solution.elf
-share/twelf/examples/prop-calc/prop-calc.elf
-share/twelf/examples/prop-calc/sources.cfg
-share/twelf/examples/prop-calc/test.cfg
-share/twelf/examples/prop-calc/thm1.elf
-share/twelf/examples/prop-calc/thm2.elf
-share/twelf/examples/prop-calc/thm3.elf
-share/twelf/examples/tabled/ccc/README
-share/twelf/examples/tabled/ccc/ccc.elf
-share/twelf/examples/tabled/ccc/tab.cfg
-share/twelf/examples/tabled/ccc/tab-examples.quy
-share/twelf/examples/tabled/README
-share/twelf/examples/tabled/all.sml
-share/twelf/examples/tabled/cr/ord-red.elf
-share/twelf/examples/tabled/cr/lam.elf
-share/twelf/examples/tabled/cr/par-red.elf
-share/twelf/examples/tabled/cr/tab-examples.quy
-share/twelf/examples/tabled/cr/tab.cfg
-share/twelf/examples/tabled/mini-ml/examples.quy
-share/twelf/examples/tabled/mini-ml/mini-ml.elf
-share/twelf/examples/tabled/mini-ml/programs.elf
-share/twelf/examples/tabled/mini-ml/reduce.elf
-share/twelf/examples/tabled/mini-ml/tab.cfg
-share/twelf/examples/tabled/mini-ml/value.elf
-share/twelf/examples/tabled/parsing/arithml.cfg
-share/twelf/examples/tabled/parsing/arithml.elf
-share/twelf/examples/tabled/parsing/arithml.quy
-share/twelf/examples/tabled/parsing/foll.cfg
-share/twelf/examples/tabled/parsing/foll.elf
-share/twelf/examples/tabled/parsing/foll.quy
-share/twelf/examples/tabled/parsing/tab.cfg
-share/twelf/examples/tabled/parsing/warren.elf
-share/twelf/examples/tabled/poly/mini-ml.elf
-share/twelf/examples/tabled/poly/tab-examples.quy
-share/twelf/examples/tabled/poly/tab.cfg
-share/twelf/examples/tabled/poly/tp.elf
-share/twelf/examples/tabled/poly/tpinf.elf
-share/twelf/examples/tabled/refine/norefex.quy
-share/twelf/examples/tabled/refine/notab.quy
-share/twelf/examples/tabled/refine/programs.elf
-share/twelf/examples/tabled/refine/refex.elf
-share/twelf/examples/tabled/refine/refex.quy
-share/twelf/examples/tabled/refine/tab.cfg
-share/twelf/examples/tabled/seqCalc/focus.elf
-share/twelf/examples/tabled/seqCalc/foc.cfg
-share/twelf/examples/tabled/seqCalc/fol-int-at.elf
-share/twelf/examples/tabled/seqCalc/formulas.elf
-share/twelf/examples/tabled/seqCalc/int-atom.elf
-share/twelf/examples/tabled/seqCalc/int.elf
-share/twelf/examples/tabled/seqCalc/sources.cfg
-share/twelf/examples/tabled/seqCalc/tab-at.cfg
-share/twelf/examples/tabled/seqCalc/tab-ex-all.quy
-share/twelf/examples/tabled/seqCalc/tab-ex-np.quy
-share/twelf/examples/tabled/seqCalc/tab-foc-all.quy
-share/twelf/examples/tabled/seqCalc/tab-fol.cfg
-share/twelf/examples/tabled/seqCalc/tab.cfg
-share/twelf/examples/tabled/subtype/mini-ml.elf
-share/twelf/examples/tabled/subtype/subtype.elf
-share/twelf/examples/tabled/subtype/tab-examples.quy
-share/twelf/examples/tabled/subtype/tab.cfg
-share/twelf/examples/tabled/subtype1/basic.elf
-share/twelf/examples/tabled/subtype1/mini-ml.elf
-share/twelf/examples/tabled/subtype1/tab-examples.quy
-share/twelf/examples/tabled/subtype1/tab.cfg
-share/twelf/examples/tabled/tests/test1.elf
-share/twelf/examples/tabled/tests/tab.cfg
-share/twelf/examples/tabled/tests/test2.elf
-share/twelf/examples/tabled/tests/test3.elf
-share/twelf/examples/tabled/tests/test4.elf
-share/twelf/examples/tabled/tests/test5.elf
-share/twelf/examples/tabled/tests/test6.elf
-share/twelf/examples/tabled/tests/test7.elf
-share/twelf/examples-clp/arith/eval.elf
-share/twelf/examples-clp/arith/examples.quy
-share/twelf/examples-clp/arith/parse.elf
-share/twelf/examples-clp/arith/sources.cfg
-share/twelf/examples-clp/arith/test.cfg
-share/twelf/examples-clp/base/base.elf
-share/twelf/examples-clp/base/examples.quy
-share/twelf/examples-clp/base/sources.cfg
-share/twelf/examples-clp/base/test.cfg
-share/twelf/examples-clp/crypt/crypt.elf
-share/twelf/examples-clp/crypt/examples.quy
-share/twelf/examples-clp/crypt/sources.cfg
-share/twelf/examples-clp/crypt/test.cfg
-share/twelf/examples-clp/integers/base.elf
-share/twelf/examples-clp/integers/cfract.elf
-share/twelf/examples-clp/integers/examples.quy
-share/twelf/examples-clp/integers/integers.elf
-share/twelf/examples-clp/integers/meta.elf
-share/twelf/examples-clp/integers/sources.cfg
-share/twelf/examples-clp/integers/test.cfg
-share/twelf/examples-clp/laplace/examples.quy
-share/twelf/examples-clp/laplace/laplace.elf
-share/twelf/examples-clp/laplace/sources.cfg
-share/twelf/examples-clp/laplace/test.cfg
-share/twelf/examples-clp/lists/examples.quy
-share/twelf/examples-clp/lists/lists.elf
-share/twelf/examples-clp/lists/sources.cfg
-share/twelf/examples-clp/lists/test.cfg
-share/twelf/examples-clp/mortgage/examples.quy
-share/twelf/examples-clp/mortgage/mortgage.elf
-share/twelf/examples-clp/mortgage/sources.cfg
-share/twelf/examples-clp/mortgage/test.cfg
-share/twelf/examples-clp/pelletier/examples.quy
-share/twelf/examples-clp/pelletier/pelletier.elf
-share/twelf/examples-clp/pelletier/sources.cfg
-share/twelf/examples-clp/pelletier/test.cfg
-share/twelf/examples-clp/sieve/examples.quy
-share/twelf/examples-clp/sieve/sieve.elf
-share/twelf/examples-clp/sieve/sieve2.elf
-share/twelf/examples-clp/sieve/sources.cfg
-share/twelf/examples-clp/sieve/test.cfg
-share/twelf/exercises/opt-eval/eval.elf
-share/twelf/exercises/opt-eval/README
-share/twelf/exercises/opt-eval/examples.quy
-share/twelf/exercises/opt-eval/mini-ml.elf
-share/twelf/exercises/opt-eval/opt-equiv1.elf
-share/twelf/exercises/opt-eval/opt-equiv1.thm
-share/twelf/exercises/opt-eval/opt-equiv2.elf
-share/twelf/exercises/opt-eval/opt-equiv2.thm
-share/twelf/exercises/opt-eval/opt-eval.elf
-share/twelf/exercises/opt-eval/opt-mini-ml.elf
-share/twelf/exercises/opt-eval/opt-rep1.elf
-share/twelf/exercises/opt-eval/opt-rep2.elf
-share/twelf/exercises/opt-eval/sources.cfg
-share/twelf/exercises/opt-eval/test.cfg
-share/twelf/exercises/README
-share/twelf/exercises/units/eqtypes.elf
-share/twelf/exercises/units/NOTES
-share/twelf/exercises/units/README
-share/twelf/exercises/units/constants.elf
-share/twelf/exercises/units/eqtype-lemmas.elf
-share/twelf/exercises/units/equnits-alg.elf
-share/twelf/exercises/units/equnits-sound.elf
-share/twelf/exercises/units/equnits.elf
-share/twelf/exercises/units/eval.elf
-share/twelf/exercises/units/examples.quy
-share/twelf/exercises/units/language.elf
-share/twelf/exercises/units/number.elf
-share/twelf/exercises/units/sources.cfg
-share/twelf/exercises/units/test.cfg
-share/twelf/exercises/units/tp-complete.elf
-share/twelf/exercises/units/tp-inf.elf
-share/twelf/exercises/units/tp-preserve.elf
-share/twelf/exercises/units/tp-rules.elf
-share/twelf/exercises/units/tp-sound.elf
-share/twelf/exercises/units/types.elf
-share/twelf/exercises/units/units.elf
-share/twelf/exercises/units/value.elf
-share/twelf/tex/code.sty
-share/twelf/tex/example.tex
-share/twelf/tex/twelf.sty
-share/twelf/vim/filetype.vim
-share/twelf/vim/README
-share/twelf/vim/syntax/twelf.vim
-@dirrm libexec/twelf/bin/.heap
-@dirrm libexec/twelf/bin
-@dirrm libexec/twelf
-@dirrm share/twelf/bin
-@dirrm share/twelf/doc/dvi
-@dirrm share/twelf/doc/html
-@dirrm share/twelf/doc/info
-@dirrm share/twelf/doc/pdf
-@dirrm share/twelf/doc/ps
-@dirrm share/twelf/doc
-@dirrm share/twelf/emacs
-@dirrm share/twelf/examples/arith
-@dirrm share/twelf/examples/ccc
-@dirrm share/twelf/examples/church-rosser
-@dirrm share/twelf/examples/compile/cls
-@dirrm share/twelf/examples/compile/cpm
-@dirrm share/twelf/examples/compile/cps
-@dirrm share/twelf/examples/compile/cxm
-@dirrm share/twelf/examples/compile/debruijn
-@dirrm share/twelf/examples/compile/debruijn1
-@dirrm share/twelf/examples/compile
-@dirrm share/twelf/examples/cpsocc
-@dirrm share/twelf/examples/cut-elim
-@dirrm share/twelf/examples/fol
-@dirrm share/twelf/examples/guide
-@dirrm share/twelf/examples/handbook
-@dirrm share/twelf/examples/incll
-@dirrm share/twelf/examples/kolm
-@dirrm share/twelf/examples/lp-horn
-@dirrm share/twelf/examples/lp
-@dirrm share/twelf/examples/mini-ml
-@dirrm share/twelf/examples/polylam
-@dirrm share/twelf/examples/prop-calc
-@dirrm share/twelf/examples/tabled/ccc
-@dirrm share/twelf/examples/tabled/cr
-@dirrm share/twelf/examples/tabled/mini-ml
-@dirrm share/twelf/examples/tabled/parsing
-@dirrm share/twelf/examples/tabled/poly
-@dirrm share/twelf/examples/tabled/refine
-@dirrm share/twelf/examples/tabled/seqCalc
-@dirrm share/twelf/examples/tabled/subtype
-@dirrm share/twelf/examples/tabled/subtype1
-@dirrm share/twelf/examples/tabled/tests
-@dirrm share/twelf/examples/tabled
-@dirrm share/twelf/examples
-@dirrm share/twelf/examples-clp/arith
-@dirrm share/twelf/examples-clp/base
-@dirrm share/twelf/examples-clp/crypt
-@dirrm share/twelf/examples-clp/integers
-@dirrm share/twelf/examples-clp/laplace
-@dirrm share/twelf/examples-clp/lists
-@dirrm share/twelf/examples-clp/mortgage
-@dirrm share/twelf/examples-clp/pelletier
-@dirrm share/twelf/examples-clp/sieve
-@dirrm share/twelf/examples-clp
-@dirrm share/twelf/exercises/opt-eval
-@dirrm share/twelf/exercises/units
-@dirrm share/twelf/exercises
-@dirrm share/twelf/tex
-@dirrm share/twelf/vim/syntax
-@dirrm share/twelf/vim
-@dirrm share/twelf