Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-06 19:51:34 -0700 (Wed, 06 Jul 2005)
Revision: 7565
Log message:

      Probably a non-working draft of lifting lemma and deduction theorem procedures
      on abstract (non-MetaPRL) Hilbert proofs.
      

Changes	Path
+1 -0	metaprl/theories/s4lp/OMakefile
Added	metaprl/theories/s4lp/hilbert_internal.ml
Properties	metaprl/theories/s4lp/hilbert_internal.ml
Added	metaprl/theories/s4lp/hilbert_internal.mli
Properties	metaprl/theories/s4lp/hilbert_internal.mli