Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-21 22:17:44 -0800 (Sun, 21 Dec 2003)
Revision: 5203
Log message:

      1.isField is now defined using ext_equal for car0 (instead of equality in a universe).
      2.I believe isField_wf is complete modulo some basic interplay between renaming and
      recordTop. Or my be I just push into a deadend.
      

Changes	Path
+8 -8	metaprl/theories/itt/itt_field.ml
+1 -1	metaprl/theories/itt/itt_field.mli
+9181 -1406	metaprl/theories/itt/itt_field.prla