Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-27 21:31:55 -0800 (Mon, 27 Feb 2006)
Revision: 8796
Log message:

      - Defined a new suffic "ta" that stands for "thenT autoT"
      - Replaced "thenT autoT", "thenWT autoT", "thenAT autoT" with "ta", "twa",
        "taa" respectively in all the *.prla and *.ml in theories.
      

Changes  Path
+3 -0 metaprl/support/tactics/auto_tactic.ml
+3 -0 metaprl/support/tactics/auto_tactic.mli
+1 -1 metaprl/theories/cic/cic_list.prla
+6 -6 metaprl/theories/czf/czf_itt_all.prla
+3 -3 metaprl/theories/czf/czf_itt_and.prla
+15 -15 metaprl/theories/czf/czf_itt_axioms.prla
+205 -205 metaprl/theories/czf/czf_itt_bool.prla
+10 -10 metaprl/theories/czf/czf_itt_coset.prla
+16 -16 metaprl/theories/czf/czf_itt_cyclic_group.prla
+6 -6 metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+22 -22 metaprl/theories/czf/czf_itt_dall.prla
+19 -19 metaprl/theories/czf/czf_itt_dexists.prla
+2 -2 metaprl/theories/czf/czf_itt_empty.prla
+33 -33 metaprl/theories/czf/czf_itt_eq.prla
+33 -33 metaprl/theories/czf/czf_itt_equiv.prla
+4 -4 metaprl/theories/czf/czf_itt_exists.prla
+3 -3 metaprl/theories/czf/czf_itt_false.prla
+14 -14 metaprl/theories/czf/czf_itt_group.prla
+6 -6 metaprl/theories/czf/czf_itt_group_bvd.prla
+13 -13 metaprl/theories/czf/czf_itt_group_power.prla
+48 -48 metaprl/theories/czf/czf_itt_hom.prla
+7 -7 metaprl/theories/czf/czf_itt_implies.prla
+8 -8 metaprl/theories/czf/czf_itt_infinity.prla
+3 -3 metaprl/theories/czf/czf_itt_inv_image.prla
+6 -6 metaprl/theories/czf/czf_itt_isect.prla
+5 -5 metaprl/theories/czf/czf_itt_iso.prla
+78 -78 metaprl/theories/czf/czf_itt_ker.prla
+1 -1 metaprl/theories/czf/czf_itt_kleingroup.prla
+18 -18 metaprl/theories/czf/czf_itt_member.prla
+36 -36 metaprl/theories/czf/czf_itt_nat.prla
+5 -5 metaprl/theories/czf/czf_itt_normal_subgroup.prla
+4 -4 metaprl/theories/czf/czf_itt_or.prla
+3 -3 metaprl/theories/czf/czf_itt_pair.prla
+13 -13 metaprl/theories/czf/czf_itt_power.prla
+1 -1 metaprl/theories/czf/czf_itt_rel.prla
+2 -2 metaprl/theories/czf/czf_itt_sall.prla
+21 -21 metaprl/theories/czf/czf_itt_sep.prla
+10 -10 metaprl/theories/czf/czf_itt_set.prla
+4 -4 metaprl/theories/czf/czf_itt_set_bvd.prla
+11 -11 metaprl/theories/czf/czf_itt_set_ind.prla
+6 -6 metaprl/theories/czf/czf_itt_setdiff.prla
+3 -3 metaprl/theories/czf/czf_itt_sexists.prla
+9 -9 metaprl/theories/czf/czf_itt_singleton.prla
+8 -8 metaprl/theories/czf/czf_itt_subgroup.prla
+3 -3 metaprl/theories/czf/czf_itt_subset.prla
+3 -3 metaprl/theories/czf/czf_itt_true.prla
+34 -34 metaprl/theories/czf/czf_itt_union.prla
+9 -9 metaprl/theories/fol/cfol_itt_all.prla
+11 -11 metaprl/theories/fol/cfol_itt_and.prla
+7 -7 metaprl/theories/fol/cfol_itt_base.prla
+1 -1 metaprl/theories/fol/fol_itt_and.prla
+2 -2 metaprl/theories/fol/fol_itt_or.prla
+1 -1 metaprl/theories/fol/fol_not.prla
+6 -6 metaprl/theories/fol/fol_prop.prla
+23 -23 metaprl/theories/itt/applications/algebra/itt_cyclic_group.prla
+14 -14 metaprl/theories/itt/applications/algebra/itt_field2.prla
+59 -59 metaprl/theories/itt/applications/algebra/itt_group.prla
+6 -6 metaprl/theories/itt/applications/algebra/itt_grouplikeobj.prla
+9 -9 metaprl/theories/itt/applications/algebra/itt_intdomain.prla
+1 -1 metaprl/theories/itt/applications/algebra/itt_mpoly2.prla
+2 -2 metaprl/theories/itt/applications/algebra/itt_mpoly2_bench.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_mpoly2_bench.prla
+2 -2 metaprl/theories/itt/applications/algebra/itt_mpoly3_bench.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_mpoly3_bench.prla
+21 -21 metaprl/theories/itt/applications/algebra/itt_poly.prla
+26 -26 metaprl/theories/itt/applications/algebra/itt_quotient_group.prla
+9 -9 metaprl/theories/itt/applications/algebra/itt_ring2.prla
+6 -6 metaprl/theories/itt/applications/algebra/itt_ring_uce.prla
+6 -6 metaprl/theories/itt/applications/algebra/itt_unitring.prla
+3 -3 metaprl/theories/itt/applications/datatypes/itt_bintree.prla
+10 -10 metaprl/theories/itt/applications/datatypes/itt_collection.prla
+88 -88 metaprl/theories/itt/applications/datatypes/itt_fset.prla
+16 -16 metaprl/theories/itt/applications/datatypes/itt_sort.prla
+5 -5 metaprl/theories/itt/applications/datatypes/itt_sortedtree.prla
+4 -4 metaprl/theories/itt/applications/function_spaces/itt_closure.prla
+6 -6 metaprl/theories/itt/applications/function_spaces/itt_functions.prla
+1 -1 metaprl/theories/itt/applications/supinf/itt_rat2.prla
+11 -11 metaprl/theories/itt/core/itt_bisect.prla
+2 -2 metaprl/theories/itt/core/itt_bool.prla
+3 -3 metaprl/theories/itt/core/itt_bunion.prla
+2 -2 metaprl/theories/itt/core/itt_decidable.prla
+3 -3 metaprl/theories/itt/core/itt_dfun.prla
+14 -14 metaprl/theories/itt/core/itt_disect.prla
+1 -1 metaprl/theories/itt/core/itt_equal.prla
+1 -1 metaprl/theories/itt/core/itt_esquash.ml
+1 -1 metaprl/theories/itt/core/itt_ext_equal.prla
+1 -1 metaprl/theories/itt/core/itt_image.prla
+5 -5 metaprl/theories/itt/core/itt_image2.prla
+1 -1 metaprl/theories/itt/core/itt_int_arith.prla
+13 -13 metaprl/theories/itt/core/itt_int_base.prla
+3 -3 metaprl/theories/itt/core/itt_int_ext.prla
+7 -7 metaprl/theories/itt/core/itt_isect.prla
+12 -12 metaprl/theories/itt/core/itt_list.prla
+96 -96 metaprl/theories/itt/core/itt_list2.prla
+1 -1 metaprl/theories/itt/core/itt_list3.prla
+14 -14 metaprl/theories/itt/core/itt_logic.prla
+33 -33 metaprl/theories/itt/core/itt_nat.prla
+1 -1 metaprl/theories/itt/core/itt_prod.prla
+8 -8 metaprl/theories/itt/core/itt_quotient.prla
+51 -51 metaprl/theories/itt/core/itt_record.prla
+3 -3 metaprl/theories/itt/core/itt_record0.ml
+26 -26 metaprl/theories/itt/core/itt_record0.prla
+19 -19 metaprl/theories/itt/core/itt_record_exm.prla
+2 -2 metaprl/theories/itt/core/itt_record_label.ml
+1 -1 metaprl/theories/itt/core/itt_record_label.prla
+7 -7 metaprl/theories/itt/core/itt_record_label0.prla
+1 -1 metaprl/theories/itt/core/itt_record_renaming.ml
+3 -3 metaprl/theories/itt/core/itt_singleton.prla
+2 -2 metaprl/theories/itt/core/itt_sqsimple.prla
+8 -8 metaprl/theories/itt/core/itt_squash.prla
+2 -2 metaprl/theories/itt/core/itt_squiggle.prla
+3 -3 metaprl/theories/itt/core/itt_struct.ml
+14 -14 metaprl/theories/itt/core/itt_struct2.prla
+4 -4 metaprl/theories/itt/core/itt_struct3.prla
+6 -6 metaprl/theories/itt/core/itt_subset.prla
+19 -19 metaprl/theories/itt/core/itt_subset2.prla
+1 -1 metaprl/theories/itt/core/itt_subtype.prla
+3 -3 metaprl/theories/itt/core/itt_tsquash.prla
+5 -5 metaprl/theories/itt/core/itt_tunion.prla
+3 -3 metaprl/theories/itt/core/itt_union.prla
+2 -2 metaprl/theories/itt/core/itt_unit.prla
+1 -1 metaprl/theories/itt/core/itt_void.prla
+2 -2 metaprl/theories/itt/core/itt_w.prla
+2 -2 metaprl/theories/itt/core/itt_well_founded.prla
+15 -15 metaprl/theories/itt/extensions/base/ctt_markov.prla
+1 -1 metaprl/theories/itt/extensions/base/itt_antiquotient.prla
+7 -7 metaprl/theories/itt/extensions/base/itt_list_sloppy.prla
+3 -3 metaprl/theories/itt/extensions/pointwise/itt_pointwise2.prla
+7 -7 metaprl/theories/itt/extensions/pointwise/itt_pointwise_struct3.prla
+7 -7 metaprl/theories/itt/extensions/rfun/itt_dfun_imp.prla
+6 -6 metaprl/theories/itt/extensions/rfun/itt_dprod_imp.prla
+3 -3 metaprl/theories/itt/extensions/rfun/itt_well_founded_equiv.prla
+1 -1 metaprl/theories/itt/extensions/vector/itt_vec_bind.prla
+3 -3 metaprl/theories/itt/extensions/vector/itt_vec_sequent_term.prla
+9 -9 metaprl/theories/itt/reflection/core/itt_hoas_debruijn.prla
+1 -1 metaprl/theories/itt/reflection/core/itt_hoas_operator.prla
+29 -29 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm.prla
+1 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
+1 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_lof.prla
+11 -11 metaprl/theories/itt/reflection/experimental/itt_hoas_proof.prla
+5 -5 metaprl/theories/itt/reflection/experimental/itt_hoas_proof_ind.prla
+13 -13 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent.prla
+10 -10 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.prla
+1 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_proof.prla
+1 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step.prla
+10 -10 metaprl/theories/itt/reflection/experimental/itt_hoas_util.prla
+4 -4 metaprl/theories/itt/reflection/experimental/jyh/itt_hoas_ulambda.prla
+50 -50 metaprl/theories/itt/reflection/obsolete/itt_hoas_lang.prla
+18 -18 metaprl/theories/itt/reflection/obsolete/itt_reflection.prla
+11 -11 metaprl/theories/itt/reflection/obsolete/itt_reflection_example_lambda.prla
+2 -2 metaprl/theories/itt/reflection/obsolete/itt_reflection_lambda_typing.prla
+11 -11 metaprl/theories/itt/reflection/obsolete/itt_synt_bterm.prla
+33 -33 metaprl/theories/itt/reflection/obsolete/itt_synt_lang.prla
+6 -6 metaprl/theories/itt/reflection/obsolete/itt_synt_operator.prla
+44 -44 metaprl/theories/itt/reflection/obsolete/itt_synt_subst.prla
+2 -2 metaprl/theories/itt/reflection/obsolete/itt_synt_var.prla
+1 -1 metaprl/theories/itt/tests/itt_int_test.prla
+2 -2 metaprl/theories/itt/tests/jprover_tests.prla
+2 -2 metaprl/theories/mesa/ma_ring__leader1_object_directory.ml
+3 -3 metaprl/theories/sil/sil_itt_sos.ml
+1 -1 metaprl/theories/tptp/tptp.prla
+3 -3 metaprl/theories/tptp/tptp_derive.prla