Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-11 08:23:32 -0700 (Wed, 11 Jul 2001)
Revision: 3326
Log message:

      - trivialT can now do equalRefT and equalSymT when necessary to match
      the conclusion with a hypothesis.
      - turned couple of Itt_equal rules from primitives into interactives
      - fixed a few FOL proofs
      - removed some obsolete files
      

Changes  Path
+2 -0 metaprl/doc/itt_quickref.txt
+13 -22 metaprl/filter/base/term_grammar.ml
+1 -1 metaprl/theories/fol/cfol_itt_base.ml
+1109 -1564 metaprl/theories/fol/cfol_itt_base.prla
Deleted metaprl/theories/fol/cfol_magic.prla
+1 -1 metaprl/theories/fol/fol_false.ml
Deleted metaprl/theories/fol/fol_type_itt.ml
Deleted metaprl/theories/fol/fol_type_itt.mli
+4 -4 metaprl/theories/itt/itt_collection.ml
+24 -13 metaprl/theories/itt/itt_equal.ml
+2 -0 metaprl/theories/itt/itt_equal.mli
+7332 -7817 metaprl/theories/itt/itt_equal.prla
+0 -12 metaprl/theories/itt/itt_esquash.ml