Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-12-28 11:55:36 -0800 (Wed, 28 Dec 2005)
Revision: 8379
Log message:

      The "thm" form is now supported.
      
         thm foo :
            sequent { <H> >- it in top } =
            "autoT"
      
      This creates an interactive theorem, where the initial rulebox
      is filled with the string "autoT".  The proof is not checked
      otherwise.