Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-02-04 16:38:18 -0800 (Sun, 04 Feb 2001)
Revision: 3140
Log message:

      
      For now 'a~'b produces Itt_squiggle!sqeq{'a;'b} rather then Perv!rewrite.
      
      I documented the Itt_squiggle theory (see all-theories.pdf).
      

Changes	Path
+0 -1	metaprl/doc/latex/theories/Makefile
+1 -0	metaprl/doc/latex/theories/itt/print.ml
+1 -2	metaprl/filter/base/term_grammar.ml
+2 -0	metaprl/theories/itt/itt_atom.ml
+1 -0	metaprl/theories/itt/itt_atom.mli
+0 -6	metaprl/theories/itt/itt_equal.ml
+0 -1	metaprl/theories/itt/itt_equal.mli
+1 -1	metaprl/theories/itt/itt_list.mli
+125 -3	metaprl/theories/itt/itt_squiggle.ml
+2 -0	metaprl/theories/itt/itt_squiggle.mli
+2 -0	metaprl/theories/itt/itt_unit.ml
+2 -2	metaprl/theories/itt/itt_unit.mli
+1 -1	metaprl/theories/tactic/nuprl_font.ml