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 |