Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-07-27 12:55:54 -0700 (Thu, 27 Jul 2000)
Revision: 3036
Log message:

      - Fixed the problem with leaking attributes.
      
      - Fixed the problem with top-level functions (such as clean_all)
      removing the "Primivive" flag and replacing it with "Interactive".
      
      - Fixed some display forms.
      
      - Removed "empty" .prla files in ITT and "refreshed" the rest of them.
      
      - More in BUGS and TODO.
      
      - Other small changes.
      

Changes  Path
+10 -3 metaprl/BUGS
+3 -2 metaprl/editor/ml/Makefile
+13 -7 metaprl/editor/ml/shell.ml
+2 -2 metaprl/editor/ml/shell_package.ml
+2 -1 metaprl/editor/ml/shell_rewrite.ml
+2 -1 metaprl/editor/ml/shell_rule.ml
+1 -1 metaprl/editor/ml/shell_sig.mlz
+34 -8 metaprl/filter/boot/proof_boot.ml
+34 -3 metaprl/filter/boot/proof_term_boot.ml
+1 -1 metaprl/theories/base/summary.ml
+430 -1256 metaprl/theories/itt/itt_bisect.prla
+1954 -6410 metaprl/theories/itt/itt_bool.prla
+310 -549 metaprl/theories/itt/itt_bunion.prla
+108 -111 metaprl/theories/itt/itt_collection.prla
+161 -189 metaprl/theories/itt/itt_decidable.prla
+2378 -2475 metaprl/theories/itt/itt_derive.prla
+1008 -1660 metaprl/theories/itt/itt_dfun.prla
+4403 -4074 metaprl/theories/itt/itt_dprod.prla
+721 -931 metaprl/theories/itt/itt_dprod_imp.prla
+8756 -7066 metaprl/theories/itt/itt_equal.prla
+935 -2039 metaprl/theories/itt/itt_esquash.prla
+2624 -3085 metaprl/theories/itt/itt_fun.prla
+1284 -1184 metaprl/theories/itt/itt_int.prla
Deleted metaprl/theories/itt/itt_int_bool.prla
+1515 -2280 metaprl/theories/itt/itt_isect.prla
+2106 -1999 metaprl/theories/itt/itt_list.prla
+958 -2721 metaprl/theories/itt/itt_list2.prla
+15901 -12661 metaprl/theories/itt/itt_logic.prla
Deleted metaprl/theories/itt/itt_prec.prla
+620 -1131 metaprl/theories/itt/itt_prod.prla
+588 -375 metaprl/theories/itt/itt_prop_decide.prla
+998 -1257 metaprl/theories/itt/itt_quotient.prla
+4633 -4520 metaprl/theories/itt/itt_rfun.prla
Deleted metaprl/theories/itt/itt_set.prla
+1795 -1857 metaprl/theories/itt/itt_sort.prla
Deleted metaprl/theories/itt/itt_squash.prla
Deleted metaprl/theories/itt/itt_srec.prla
+2346 -2130 metaprl/theories/itt/itt_struct.prla
+2783 -3112 metaprl/theories/itt/itt_subtype.prla
Deleted metaprl/theories/itt/itt_theory.prla
Deleted metaprl/theories/itt/itt_tunion.prla
+3724 -3185 metaprl/theories/itt/itt_union.prla
Deleted metaprl/theories/itt/itt_unit.prla
Deleted metaprl/theories/itt/itt_void.prla
Deleted metaprl/theories/itt/itt_w.prla
+402 -451 metaprl/theories/itt/itt_well_founded.prla