Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-05 20:40:58 -0800 (Sat, 05 Nov 2005)
Revision: 8111
Log message:

      Added the "reflected_logic" block, see Pmn_core_logic for an example.
      Currently working out the rule arguments, so the final few
      rules are disabled.
      
      The main goal is, for a rule
      
         interactive foo : <mt>
      
      Do 3 things:
         1. Define unfold_foo : foo <--> <mt>
         2. Add a wf rule, <H> >- foo IN ProofRule
         3. Add the provability rule (one direction of reflection):
      
            If <mt> == <t1> --> ... -> <tn>
            Add the real rule:
      
               <H> -> Provable{t1} -->
               ...
               <H> -> Provable{tn}