Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-11-17 21:25:05 -0800 (Wed, 17 Nov 2004)
Revision: 6274
Log message:

      Fixing some of the proofs broken by today's reflection changes.
      Xin, I am leaving the rest of them to you.
      

Changes  Path
+0 -2 metaprl/theories/itt/itt_fun.ml
+3 -0 metaprl/theories/itt/itt_nat.ml
+1560 -1364 metaprl/theories/itt/itt_nat.prla
+3 -1 metaprl/theories/itt/itt_reflection.ml
+3169 -2943 metaprl/theories/itt/itt_reflection.prla