Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-04-13 16:26:25 -0700 (Thu, 13 Apr 2000)
Revision: 2934
Log message:

      I started writing a formal description of the syntax of sequent schemas
      that are used in rule specifications and when proving derived rules.
      
      I am planning to give a formal definition of what it means for a sequent
      specification to be a refinement of another sequent specification.
      
      After that I am going to start proving that the way we use rules on sequent
      schemas instead of ordinary sequents when proving derived rules is valid.
      Since under the current implementation it is _not_ completely valid,
      I will only sketch a proof, but this should be enough to understand
      what we need to add to make it completely valid.
      

Changes	Path
+2 -0	metaprl/doc/htmlman/user-guide/mp-axiom.html