Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-10-06 23:04:10 -0700 (Thu, 06 Oct 2005)
Revision: 7871
Log message:

      Removing the Itt_fun module. Now the independent function is just a dependent
      function where the dependency variable does not occur (and will normally be
      represented by an empty string).
      

Changes  Path
+6 -1 metaprl/filter/filter/term_grammar.ml
+20 -0 metaprl/refiner/refiner/refiner_debug.ml
+4 -0 metaprl/refiner/refsig/term_op_sig.ml
+27 -0 metaprl/refiner/term_ds/term_op_ds.ml
+1 -1 metaprl/refiner/term_gen/term_meta_gen.ml
+25 -0 metaprl/refiner/term_std/term_op_std.ml
+5 -0 metaprl/support/display/base_dform.ml
+2 -0 metaprl/support/display/base_dform.mli
+6 -4 metaprl/theories/czf/czf_itt_all.prla
+9 -5 metaprl/theories/czf/czf_itt_axioms.prla
+2 -1 metaprl/theories/czf/czf_itt_bool.prla
+4 -3 metaprl/theories/czf/czf_itt_dall.prla
+2 -1 metaprl/theories/czf/czf_itt_dexists.prla
+6 -4 metaprl/theories/czf/czf_itt_eq.prla
+6 -4 metaprl/theories/czf/czf_itt_exists.prla
+2 -2 metaprl/theories/czf/czf_itt_fol.mlz
+4 -4 metaprl/theories/czf/czf_itt_implies.ml
+10 -5 metaprl/theories/czf/czf_itt_implies.prla
+4 -3 metaprl/theories/czf/czf_itt_member.prla
+4 -3 metaprl/theories/czf/czf_itt_nat.prla
+3 -3 metaprl/theories/czf/czf_itt_power.ml
+10 -6 metaprl/theories/czf/czf_itt_power.prla
+4 -3 metaprl/theories/czf/czf_itt_sep.prla
+10 -8 metaprl/theories/czf/czf_itt_set.prla
+3 -2 metaprl/theories/czf/czf_itt_set_bvd.prla
+3 -2 metaprl/theories/czf/czf_itt_set_ind.prla
+6 -5 metaprl/theories/czf/czf_itt_union.prla
+1 -1 metaprl/theories/fol/fol_itt_implies.ml
+2 -1 metaprl/theories/fol/fol_itt_implies.prla
+0 -1 metaprl/theories/itt/OMakefile
+18 -13 metaprl/theories/itt/itt_closure.prla
+0 -1 metaprl/theories/itt/itt_collection.ml
+0 -1 metaprl/theories/itt/itt_collection.mli
+6 -4 metaprl/theories/itt/itt_collection.prla
+8 -14 metaprl/theories/itt/itt_comment.ml
+2 -3 metaprl/theories/itt/itt_comment.mli
+12 -6 metaprl/theories/itt/itt_cyclic_group.prla
+0 -1 metaprl/theories/itt/itt_derive.ml
+0 -1 metaprl/theories/itt/itt_derive.mli
+2 -1 metaprl/theories/itt/itt_derive.prla
+51 -7 metaprl/theories/itt/itt_dfun.ml
+3 -1 metaprl/theories/itt/itt_dfun.mli
+4996 -4086 metaprl/theories/itt/itt_dfun.prla
+1 -1 metaprl/theories/itt/itt_disect.ml
+2 -2 metaprl/theories/itt/itt_dprod.ml
+0 -1 metaprl/theories/itt/itt_dprod_imp.ml
+2 -5 metaprl/theories/itt/itt_eta.ml
+1 -1 metaprl/theories/itt/itt_eta.mli
+4 -3 metaprl/theories/itt/itt_eta.prla
+40 -20 metaprl/theories/itt/itt_field2.prla
+109 -61 metaprl/theories/itt/itt_field_e.prla
+1 -1 metaprl/theories/itt/itt_fset.ml
+1 -1 metaprl/theories/itt/itt_fset.mli
+9 -5 metaprl/theories/itt/itt_fset.prla
Deleted metaprl/theories/itt/itt_fun.ml
Deleted metaprl/theories/itt/itt_fun.mli
Deleted metaprl/theories/itt/itt_fun.prla
+5 -5 metaprl/theories/itt/itt_fun2.ml
+1 -1 metaprl/theories/itt/itt_fun2.mli
+14 -8 metaprl/theories/itt/itt_fun2.prla
+15 -9 metaprl/theories/itt/itt_functions.prla
+70 -35 metaprl/theories/itt/itt_group.prla
+2 -2 metaprl/theories/itt/itt_grouplikeobj.ml
+1 -1 metaprl/theories/itt/itt_grouplikeobj.mli
+16 -8 metaprl/theories/itt/itt_grouplikeobj.prla
+1 -1 metaprl/theories/itt/itt_hoas_base.ml
+2 -1 metaprl/theories/itt/itt_hoas_lang.prla
+1 -1 metaprl/theories/itt/itt_image.ml
+0 -1 metaprl/theories/itt/itt_int_arith.mli
+0 -1 metaprl/theories/itt/itt_int_base.mli
+0 -1 metaprl/theories/itt/itt_int_ext.mli
+1 -1 metaprl/theories/itt/itt_isect.ml
+0 -1 metaprl/theories/itt/itt_isect.mli
+2 -1 metaprl/theories/itt/itt_isect.prla
+1 -0 metaprl/theories/itt/itt_list2.ml
+1 -0 metaprl/theories/itt/itt_list2.mli
+24 -16 metaprl/theories/itt/itt_list2.prla
+3 -6 metaprl/theories/itt/itt_logic.ml
+0 -1 metaprl/theories/itt/itt_logic.mli
+12 -7 metaprl/theories/itt/itt_logic.prla
+2 -1 metaprl/theories/itt/itt_mpoly2.prla
+17 -10 metaprl/theories/itt/itt_order.prla
+16 -14 metaprl/theories/itt/itt_poly.prla
+1 -1 metaprl/theories/itt/itt_prec.ml
+1 -1 metaprl/theories/itt/itt_prec.mli
+5 -3 metaprl/theories/itt/itt_quotient.prla
+17 -9 metaprl/theories/itt/itt_quotient_group.prla
+0 -1 metaprl/theories/itt/itt_rat.mli
+1 -1 metaprl/theories/itt/itt_record_exm.ml
+1 -1 metaprl/theories/itt/itt_record_exm.mli
+24 -13 metaprl/theories/itt/itt_record_exm.prla
+1 -1 metaprl/theories/itt/itt_reflection_lambda_typing.ml
+2 -1 metaprl/theories/itt/itt_reflection_lambda_typing.prla
+26 -20 metaprl/theories/itt/itt_rfun.ml
+3 -2 metaprl/theories/itt/itt_rfun.mli
+2 -1 metaprl/theories/itt/itt_rfun.prla
+1 -1 metaprl/theories/itt/itt_ring2.ml
+16 -8 metaprl/theories/itt/itt_ring2.prla
+20 -12 metaprl/theories/itt/itt_ring_e.prla
+25 -15 metaprl/theories/itt/itt_ring_uce.prla
+7 -4 metaprl/theories/itt/itt_sort.prla
+2 -1 metaprl/theories/itt/itt_subset.prla
+5 -3 metaprl/theories/itt/itt_subset2.prla
+4 -2 metaprl/theories/itt/itt_synt_lang.prla
+0 -1 metaprl/theories/itt/itt_theory.ml
+0 -1 metaprl/theories/itt/itt_theory.mli
+10 -5 metaprl/theories/itt/itt_tunion.prla
+40 -24 metaprl/theories/itt/itt_unitring.prla
+2 -2 metaprl/theories/itt/itt_w.ml
+4 -3 metaprl/theories/itt/itt_w.prla
+1 -1 metaprl/theories/itt/itt_well_founded.ml
+1 -1 metaprl/theories/itt/itt_well_founded.mli
+3 -2 metaprl/theories/itt/itt_well_founded.prla
+20 -10 metaprl/theories/tptp/tptp.prla