Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-28 18:59:35 -0800 (Sat, 28 Jan 2006)
Revision: 8619
Log message:

      Manually branch the reflection/experimental directory
      to reflection/experimental_bsequent.  This is mainly
      so that we can keep the proofs for copying purposes.
      I will delete the experimental_bsequent directory if
      everything works out, or restore it if things do not.
      
      Plan is to investigate "append sequents".  Roughly
      speaking the new sequent will have the form:
      
         asequent{| <H>; x: hyp{A}; y: J[x] >- C[x; y] |}
      
      where 
      
         <H> represents a list of lists
         hyp{'A} <--> ['A]
         'J['x] represents a list
      
      Lots of issues that need to be solved, we'll see how it goes.
      

Changes  Path
Copied metaprl/theories/itt/reflection/experimental_bsequent