Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-22 17:41:51 -0800 (Tue, 22 Nov 2005)
Revision: 8200
Log message:
The basic meta_dT works, but I haven't corrected the
resource annotations yet.
The extracts are currently wrong. I have to figure out
the arguments to the extract function (like what a
subgoal extract looks like).
Changes | Path |
+9 -2 | metaprl/theories/extensions/meta_implies.ml |
Added | metaprl/theories/extensions/meta_implies.prla |
Properties | metaprl/theories/extensions/meta_implies.prla |