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