Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-23 08:42:53 -0700 (Wed, 23 May 2001)
Revision: 3236
Log message:

      - Proved all the theorems in itt_squash.
      - Still need to figure out the right way to do squash_resource and
      the relevant tactics.
      

Changes  Path
+2 -1 metaprl/theories/itt/itt_bool.ml
+0 -3 metaprl/theories/itt/itt_equal.ml
+0 -2 metaprl/theories/itt/itt_equal.mli
+111 -66 metaprl/theories/itt/itt_squash.ml
+26 -16 metaprl/theories/itt/itt_squash.mli
Added metaprl/theories/itt/itt_squash.prla
Properties metaprl/theories/itt/itt_squash.prla
+3 -1 metaprl/theories/tactic/nuprl_font.ml