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 |