            Hints on proving theorems in Twelf
                  Andrew W. Appel
                  February 2000


To run this tutorial, use Emacs to visit the file  proving.elf  
  in this directory.  If Emacs seems to freeze with "fontifying proving.elf"
  just type control-G to stop the fontification and let you read the
  unfontified file.

Contents:

proving.elf    
  1.  The mechanics of running Twelf.
  2.  Proving a theorem.
  3.  Organization of the object logic.
  4.  Examples using and, and_i, and_l.
  5.  Proof style.

proving2.elf
  6.  Implication elimination and introduction; metalogic vs. object logic.
  7.  Or, false, not.

proving3.elf 
  8.  Twelf metalogic quantification.
  9.  Types in the object logic.
 10.  Creating object-logic functions and predicates.
 11.  Object logic quantification.

proving4.elf
 12.  Equality and congruence
 13.  Forward proof using "cut"
 14.  Twelf Traps and pitfalls
 15.  Object-logic definitions

proving5.elf 
 16.  A case study

proving6.elf
 17.  Coping with nonstrictness
 18.  A case study in strictness and type inference (by Kedar Swadi)

proving7.elf
 19.  Extensionality & Equivalence Relations
