Twelf
Copyright (C) 1997-2002, Frank Pfenning and Carsten Schuermann

Authors: Frank Pfenning
         Carsten Schuermann
With contributions by:
         Brigitte Pientka
         Roberto Virga
         Kevin Watkins
         Jason Reed
         Robert J. Simmons

Twelf is an implementation of

 - the LF logical framework, including type reconstruction
 - the Elf constraint logic programming language
 - a meta-theorem prover for LF (very preliminary)
 - a set of expansion modules to deal natively with numbers and strings
 - an Emacs interface

For installation instructions, see http://twelf.org/

Twelf can be compiled and installed under Unix, either as a separate
"Twelf Server" intended primarily as an inferior process to Emacs, or as
a structure Twelf embedded in Standard ML.

Files
=====

 README            --- this file
 Makefile          --- enables make
 server.cm         --- used to build Twelf Server
 sources.cm        --- used to build Twelf SML
 bin/              --- utility scripts, heaps, binaries
 build/            --- build files (type "make" to see options)
 doc/              --- (Outdated) Twelf user's guide
 emacs/            --- Emacs interface for Twelf
 examples/         --- various case studies
 examples-clp/     --- examples of use of the numbers and strings extensions
 src/              --- the SML sources for Twelf
 tex/              --- TeX macros and style files
 vim/              --- Vim interface for Twelf