Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-06 20:45:56 -0800 (Sun, 06 Feb 2005)
Revision: 6612
Log message:

      - I've added a "docon" term that is the opposite of the "docoff". One can now
        write simply
           doc docon
        instead of having to do something like
           doc <:doc< @doc{ } >>
      
      - I've added "doc docoff"/"doc docon" in a few places in ITT to exclude ML
        code from the theories.pdf file (I did this some of the theories that needed
        it, but most likely not in all of them).
      

Changes  Path
+16 -9 metaprl/support/display/comment.ml
+1 -0 metaprl/support/display/comment.mli
+7 -8 metaprl/theories/itt/itt_bisect.ml
+5 -3 metaprl/theories/itt/itt_bunion.ml
+15 -4 metaprl/theories/itt/itt_collection.ml
+1 -0 metaprl/theories/itt/itt_decidable.ml
+1 -1 metaprl/theories/itt/itt_disect.ml
+1 -1 metaprl/theories/itt/itt_equal.ml
+2 -2 metaprl/theories/itt/itt_field2.ml
+2 -1 metaprl/theories/itt/itt_field_e.ml
+1 -1 metaprl/theories/itt/itt_int_arith.ml
+6 -5 metaprl/theories/itt/itt_isect.ml
+7 -0 metaprl/theories/itt/itt_order.ml
+18 -5 metaprl/theories/itt/itt_record.ml
+19 -13 metaprl/theories/itt/itt_record_exm.ml
+8 -4 metaprl/theories/itt/itt_record_renaming.ml
+3 -1 metaprl/theories/itt/itt_relation_str.ml
+3 -5 metaprl/theories/itt/itt_ring2.ml
+1 -1 metaprl/theories/itt/itt_ring_e.ml
+1 -1 metaprl/theories/itt/itt_ring_uce.ml
+5 -3 metaprl/theories/itt/itt_tunion.ml
+1 -1 metaprl/theories/itt/itt_unitring.ml