Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-06-19 08:17:10 -0700 (Tue, 19 Jun 2001)
Revision: 3276
Log message:

      Added support for the following syntax of resource improvement:
      let resource name += expr
      and
      let resource name += [ expr1; expr2; ...; exprn ]
      

Changes  Path
+3 -0 metaprl/editor/ml/shell.ml
+1 -1 metaprl/editor/ml/shell_package.ml
+63 -24 metaprl/filter/base/filter_prog.ml
+1 -0 metaprl/filter/base/filter_prog.mli
+43 -48 metaprl/filter/base/filter_summary.ml
+8 -0 metaprl/filter/base/filter_type.ml
+11 -0 metaprl/filter/filter/filter_parse.ml
+0 -3 metaprl/refiner/reflib/ascii_io.ml
+5 -0 metaprl/refiner/reflib/mp_resource.ml
+1 -0 metaprl/refiner/reflib/mp_resource.mli
Properties metaprl/theories/base
+10 -12 metaprl/theories/base/base_auto_tactic.ml
+5 -14 metaprl/theories/base/base_dtactic.ml
+0 -4 metaprl/theories/base/base_dtactic.mli
+5 -6 metaprl/theories/base/base_rewrite.ml
+1 -3 metaprl/theories/czf/czf_itt_dall.ml
+2 -3 metaprl/theories/czf/czf_itt_dexists.ml
+14 -18 metaprl/theories/czf/czf_itt_eq.ml
+2 -6 metaprl/theories/czf/czf_itt_member.ml
+2 -3 metaprl/theories/czf/czf_itt_power.ml
+1 -3 metaprl/theories/czf/czf_itt_sep.ml
+8 -10 metaprl/theories/czf/czf_itt_set.ml
+4 -4 metaprl/theories/czf/czf_itt_set_ind.ml
+2 -3 metaprl/theories/czf/czf_itt_union.ml
+2 -2 metaprl/theories/fol/fol_bisect_itt.ml
+2 -9 metaprl/theories/fol/fol_false.ml
+5 -6 metaprl/theories/fol/fol_pred.ml
+5 -6 metaprl/theories/fol/fol_struct.ml
+5 -6 metaprl/theories/fol/fol_univ.ml
+3 -3 metaprl/theories/fol/fol_univ_itt.ml
+2 -3 metaprl/theories/itt/itt_atom.ml
+3 -3 metaprl/theories/itt/itt_bisect.ml
+9 -11 metaprl/theories/itt/itt_bool.ml
+9 -18 metaprl/theories/itt/itt_collection.ml
+2 -5 metaprl/theories/itt/itt_dfun.ml
+2 -5 metaprl/theories/itt/itt_disect.ml
+7 -13 metaprl/theories/itt/itt_dprod.ml
+4 -9 metaprl/theories/itt/itt_dprod_imp.ml
+10 -15 metaprl/theories/itt/itt_equal.ml
+1 -1 metaprl/theories/itt/itt_esquash.ml
+17 -37 metaprl/theories/itt/itt_fset.ml
+5 -8 metaprl/theories/itt/itt_fun.ml
+4 -6 metaprl/theories/itt/itt_int.ml
+3 -5 metaprl/theories/itt/itt_int_base.ml
+1 -2 metaprl/theories/itt/itt_int_bool.ml
+1 -2 metaprl/theories/itt/itt_int_ext.ml
+2 -5 metaprl/theories/itt/itt_isect.ml
+6 -10 metaprl/theories/itt/itt_list.ml
+3 -4 metaprl/theories/itt/itt_list2.ml
+29 -40 metaprl/theories/itt/itt_logic.ml
+2 -2 metaprl/theories/itt/itt_prec.ml
+2 -5 metaprl/theories/itt/itt_prod.ml
+2 -5 metaprl/theories/itt/itt_quotient.ml
+10 -15 metaprl/theories/itt/itt_record.ml
+7 -11 metaprl/theories/itt/itt_record0.ml
+2 -5 metaprl/theories/itt/itt_record_exm.ml
+2 -5 metaprl/theories/itt/itt_record_label.ml
+1 -2 metaprl/theories/itt/itt_record_label0.ml
+4 -5 metaprl/theories/itt/itt_rfun.ml
+2 -6 metaprl/theories/itt/itt_set.ml
+1 -2 metaprl/theories/itt/itt_sort.ml
+13 -22 metaprl/theories/itt/itt_squash.ml
+2 -2 metaprl/theories/itt/itt_srec.ml
+10 -12 metaprl/theories/itt/itt_struct.ml
+2 -3 metaprl/theories/itt/itt_subtype.ml
+1 -3 metaprl/theories/itt/itt_test.ml
+4 -4 metaprl/theories/itt/itt_tsub.ml
+6 -10 metaprl/theories/itt/itt_union.ml
+2 -3 metaprl/theories/itt/itt_unit.ml
+2 -5 metaprl/theories/itt/itt_void.ml
+4 -6 metaprl/theories/itt/itt_w.ml
+6 -0 metaprl/theories/tactic/summary.ml
+0 -5 metaprl/theories/tactic/top_conversionals.ml
+0 -4 metaprl/theories/tactic/top_conversionals.mli
+6 -7 metaprl/theories/tptp/tptp.ml