Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 19:55:14 -0800 (Tue, 22 Nov 2005)
Revision: 8202
Log message:

      Added the structural rules for the meta-logic, including cut and thinning.
      
      Unfortunately, these rules are ML rules, but only because we can't
      express the extract properly.
      
      Yes I know, meta-logical power is like a siren, and we can become
      entralled by her beauty--to our own peril.
      
      Still it would be cool if we could write down this stuff the right
      way.  For example, thinning.
      
         <H>; <J> --> E
         -----------------
         <H>; A; <J> --> E
      
      Here, <H> and <J> correspond to lists of assumptions.
      Crazy, yes.  At least they are not dependent:/
      

Changes  Path
+5 -0 metaprl/theories/extensions/meta_implies.mli
+53 -1 metaprl/theories/extensions/meta_struct.ml
+3 -0 metaprl/theories/extensions/meta_struct.mli