Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 21:58:37 -0700 (Thu, 01 May 2003)
Revision: 4541
Log message:

      Moved and renamed:
      theories/base/typeinf -> support/tactics/typeinf
      theories/base/base_auto_tactic -> support/tactics/auto_tactic
      theories/base/base_dtactic -> support/tactics/dtactic
      
      P.S. This is the "tail" of the commit - previous commit failed half-way
      through :-( Turns out that if you simultaneously run "cvs commit" and
      "cvs update" on a single tree (from different machines over NFS),
      they will fight...
      

Changes  Path
+2 -2 metaprl/theories/czf/czf_itt_nat.prla
+2 -2 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+2 -2 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+2 -2 metaprl/theories/czf/czf_itt_normal_subgroup.prla
+1 -1 metaprl/theories/czf/czf_itt_or.ml
+2 -2 metaprl/theories/czf/czf_itt_or.prla
+1 -1 metaprl/theories/czf/czf_itt_pair.ml
+2 -2 metaprl/theories/czf/czf_itt_pair.prla
+1 -1 metaprl/theories/czf/czf_itt_power.ml
+2 -2 metaprl/theories/czf/czf_itt_power.prla
+2 -2 metaprl/theories/czf/czf_itt_pre_theory.prla
+1 -1 metaprl/theories/czf/czf_itt_rel.ml
+2 -2 metaprl/theories/czf/czf_itt_rel.prla
+1 -1 metaprl/theories/czf/czf_itt_sall.ml
+2 -2 metaprl/theories/czf/czf_itt_sall.prla
+1 -1 metaprl/theories/czf/czf_itt_sep.ml
+2 -2 metaprl/theories/czf/czf_itt_sep.prla
+2 -2 metaprl/theories/czf/czf_itt_set.ml
+1 -1 metaprl/theories/czf/czf_itt_set.mli
+2 -2 metaprl/theories/czf/czf_itt_set.prla
+2 -2 metaprl/theories/czf/czf_itt_set_bvd.ml
+2 -2 metaprl/theories/czf/czf_itt_set_bvd.mli
+2 -2 metaprl/theories/czf/czf_itt_set_bvd.prla
+1 -1 metaprl/theories/czf/czf_itt_set_ind.ml
+2 -2 metaprl/theories/czf/czf_itt_set_ind.prla
+2 -2 metaprl/theories/czf/czf_itt_setdiff.ml
+2 -2 metaprl/theories/czf/czf_itt_setdiff.mli
+2 -2 metaprl/theories/czf/czf_itt_setdiff.prla
+1 -1 metaprl/theories/czf/czf_itt_sexists.ml
+2 -2 metaprl/theories/czf/czf_itt_sexists.prla
+1 -1 metaprl/theories/czf/czf_itt_singleton.ml
+2 -2 metaprl/theories/czf/czf_itt_singleton.prla
+2 -2 metaprl/theories/czf/czf_itt_subgroup.ml
+2 -2 metaprl/theories/czf/czf_itt_subgroup.mli
+2 -2 metaprl/theories/czf/czf_itt_subgroup.prla
+1 -1 metaprl/theories/czf/czf_itt_subset.ml
+2 -2 metaprl/theories/czf/czf_itt_subset.prla
+1 -1 metaprl/theories/czf/czf_itt_true.ml
+2 -2 metaprl/theories/czf/czf_itt_true.prla
+1 -1 metaprl/theories/czf/czf_itt_union.ml
+2 -2 metaprl/theories/czf/czf_itt_union.prla
+2 -2 metaprl/theories/fir/mfir_auto.ml
+1 -1 metaprl/theories/fir/mfir_auto.mli
+2 -2 metaprl/theories/fir/mfir_test.prla
+2 -2 metaprl/theories/fol/cfol_itt_all.prla
+1 -1 metaprl/theories/fol/cfol_itt_and.ml
+2 -2 metaprl/theories/fol/cfol_itt_and.prla
+1 -1 metaprl/theories/fol/cfol_itt_base.ml
+2 -2 metaprl/theories/fol/cfol_itt_base.prla
+1 -1 metaprl/theories/fol/fol_all.ml
+1 -1 metaprl/theories/fol/fol_and.ml
+2 -2 metaprl/theories/fol/fol_ctheory.prla
+1 -1 metaprl/theories/fol/fol_exists.ml
+1 -1 metaprl/theories/fol/fol_false.ml
+1 -1 metaprl/theories/fol/fol_implies.ml
+2 -2 metaprl/theories/fol/fol_itt_and.prla
+2 -2 metaprl/theories/fol/fol_itt_false.prla
+2 -2 metaprl/theories/fol/fol_itt_implies.prla
+2 -2 metaprl/theories/fol/fol_itt_or.prla
+2 -2 metaprl/theories/fol/fol_itt_true.prla
+1 -1 metaprl/theories/fol/fol_not.ml
+2 -2 metaprl/theories/fol/fol_not.prla
+1 -1 metaprl/theories/fol/fol_or.ml
+1 -1 metaprl/theories/fol/fol_pred.ml
+2 -2 metaprl/theories/fol/fol_prop.ml
+2 -2 metaprl/theories/fol/fol_prop.prla
+1 -1 metaprl/theories/fol/fol_struct.ml
+1 -1 metaprl/theories/fol/fol_true.ml
+1 -1 metaprl/theories/fol/fol_univ.ml
+1 -1 metaprl/theories/itt/ctt_markov.ml
+2 -2 metaprl/theories/itt/ctt_markov.prla
+1 -1 metaprl/theories/itt/itt_algebra_df.ml
+2 -2 metaprl/theories/itt/itt_antiquotient.prla
+1 -1 metaprl/theories/itt/itt_atom.ml
+1 -1 metaprl/theories/itt/itt_atom_bool.ml
+2 -2 metaprl/theories/itt/itt_bintree.ml
+2 -2 metaprl/theories/itt/itt_bintree.mli
+2 -2 metaprl/theories/itt/itt_bintree.prla
+1 -1 metaprl/theories/itt/itt_bisect.ml
+2 -2 metaprl/theories/itt/itt_bisect.prla
+2 -2 metaprl/theories/itt/itt_bool.ml
+2 -2 metaprl/theories/itt/itt_bool.prla
+2 -2 metaprl/theories/itt/itt_bugs.prla
+1 -1 metaprl/theories/itt/itt_bunion.ml
+2 -2 metaprl/theories/itt/itt_bunion.prla
+2 -2 metaprl/theories/itt/itt_collection.ml
+2 -2 metaprl/theories/itt/itt_collection.prla
+2 -2 metaprl/theories/itt/itt_cyclic_group.ml
+2 -2 metaprl/theories/itt/itt_cyclic_group.mli
+2 -2 metaprl/theories/itt/itt_cyclic_group.prla
+2 -2 metaprl/theories/itt/itt_datatree.ml
+2 -2 metaprl/theories/itt/itt_decidable.ml
+2 -2 metaprl/theories/itt/itt_decidable.prla
+2 -2 metaprl/theories/itt/itt_derive.prla
+1 -1 metaprl/theories/itt/itt_dfun.ml
+2 -2 metaprl/theories/itt/itt_dfun.prla
+2 -2 metaprl/theories/itt/itt_disect.ml
+2 -2 metaprl/theories/itt/itt_disect.prla
+1 -1 metaprl/theories/itt/itt_dprod.ml
+2 -2 metaprl/theories/itt/itt_dprod.prla
+1 -1 metaprl/theories/itt/itt_dprod_imp.ml
+2 -2 metaprl/theories/itt/itt_dprod_imp.prla
+2 -2 metaprl/theories/itt/itt_equal.ml
+1 -1 metaprl/theories/itt/itt_equal.mli
+2 -2 metaprl/theories/itt/itt_equal.prla
+2 -2 metaprl/theories/itt/itt_esquash.ml
+2 -2 metaprl/theories/itt/itt_esquash.prla
+1 -1 metaprl/theories/itt/itt_example.ml
+1 -1 metaprl/theories/itt/itt_ext_equal.ml
+2 -2 metaprl/theories/itt/itt_ext_equal.prla
+2 -2 metaprl/theories/itt/itt_fset.ml
+2 -2 metaprl/theories/itt/itt_fset.prla
+1 -1 metaprl/theories/itt/itt_fun.ml
+2 -2 metaprl/theories/itt/itt_fun.prla
+2 -2 metaprl/theories/itt/itt_group.ml
+2 -2 metaprl/theories/itt/itt_group.mli
+2 -2 metaprl/theories/itt/itt_group.prla
+2 -2 metaprl/theories/itt/itt_grouplikeobj.ml
+2 -2 metaprl/theories/itt/itt_grouplikeobj.mli
+2 -2 metaprl/theories/itt/itt_grouplikeobj.prla
+1 -1 metaprl/theories/itt/itt_int_arith.ml
+2 -2 metaprl/theories/itt/itt_int_arith.prla
+2 -2 metaprl/theories/itt/itt_int_base.ml
+2 -2 metaprl/theories/itt/itt_int_base.prla
+2 -2 metaprl/theories/itt/itt_int_ext.ml
+2 -2 metaprl/theories/itt/itt_int_ext.prla
+2 -2 metaprl/theories/itt/itt_inv_typing.ml
+2 -2 metaprl/theories/itt/itt_inv_typing.mli
+1 -1 metaprl/theories/itt/itt_isect.ml
+2 -2 metaprl/theories/itt/itt_isect.prla
+1 -1 metaprl/theories/itt/itt_list.ml
+2 -2 metaprl/theories/itt/itt_list.prla
+1 -1 metaprl/theories/itt/itt_list2.ml
+2 -2 metaprl/theories/itt/itt_list2.prla
+2 -2 metaprl/theories/itt/itt_logic.ml
+1 -1 metaprl/theories/itt/itt_logic.mli
+2 -2 metaprl/theories/itt/itt_logic.prla
+2 -2 metaprl/theories/itt/itt_nat.ml
+2 -2 metaprl/theories/itt/itt_nat.prla
+1 -1 metaprl/theories/itt/itt_pointwise.ml
+2 -2 metaprl/theories/itt/itt_pointwise.prla
+2 -2 metaprl/theories/itt/itt_pointwise2.ml
+2 -2 metaprl/theories/itt/itt_pointwise2.prla
+1 -1 metaprl/theories/itt/itt_prec.ml
+1 -1 metaprl/theories/itt/itt_prod.ml
+2 -2 metaprl/theories/itt/itt_prod.prla
+2 -2 metaprl/theories/itt/itt_prop_decide.ml
+2 -2 metaprl/theories/itt/itt_prop_decide.prla
+1 -1 metaprl/theories/itt/itt_quotient.ml
+2 -2 metaprl/theories/itt/itt_quotient.prla
+2 -2 metaprl/theories/itt/itt_rbtree.ml
+2 -2 metaprl/theories/itt/itt_record.ml
+2 -2 metaprl/theories/itt/itt_record.prla
+1 -1 metaprl/theories/itt/itt_record0.ml
+2 -2 metaprl/theories/itt/itt_record0.prla
+1 -1 metaprl/theories/itt/itt_record_exm.ml
+2 -2 metaprl/theories/itt/itt_record_exm.prla
+3 -3 metaprl/theories/itt/itt_record_label.ml
+2 -2 metaprl/theories/itt/itt_record_label.prla
+1 -1 metaprl/theories/itt/itt_record_label0.ml
+2 -2 metaprl/theories/itt/itt_record_label0.prla
+2 -2 metaprl/theories/itt/itt_relation_str.ml
+1 -1 metaprl/theories/itt/itt_rfun.ml
+2 -2 metaprl/theories/itt/itt_rfun.prla
+1 -1 metaprl/theories/itt/itt_set.ml
+2 -2 metaprl/theories/itt/itt_set.prla
+2 -2 metaprl/theories/itt/itt_set_str.ml
+2 -2 metaprl/theories/itt/itt_singleton.ml
+2 -2 metaprl/theories/itt/itt_singleton.prla
+1 -1 metaprl/theories/itt/itt_sort.ml
+2 -2 metaprl/theories/itt/itt_sort.prla
+2 -2 metaprl/theories/itt/itt_sortedtree.ml
+2 -2 metaprl/theories/itt/itt_sortedtree.prla
+2 -2 metaprl/theories/itt/itt_squash.ml
+2 -2 metaprl/theories/itt/itt_squash.prla
+1 -1 metaprl/theories/itt/itt_squiggle.ml
+2 -2 metaprl/theories/itt/itt_squiggle.prla
+1 -1 metaprl/theories/itt/itt_srec.ml
+1 -1 metaprl/theories/itt/itt_struct.ml
+2 -2 metaprl/theories/itt/itt_struct.prla
+2 -2 metaprl/theories/itt/itt_struct2.ml
+2 -2 metaprl/theories/itt/itt_struct2.prla
+1 -1 metaprl/theories/itt/itt_struct3.ml
+1 -1 metaprl/theories/itt/itt_struct3.mli
+2 -2 metaprl/theories/itt/itt_struct3.prla
+2 -2 metaprl/theories/itt/itt_subset.ml
+2 -2 metaprl/theories/itt/itt_subset.prla
+2 -2 metaprl/theories/itt/itt_subset2.ml
+2 -2 metaprl/theories/itt/itt_subset2.prla
+1 -1 metaprl/theories/itt/itt_subtype.ml
+2 -2 metaprl/theories/itt/itt_subtype.prla
+1 -1 metaprl/theories/itt/itt_tsquash.ml
+2 -2 metaprl/theories/itt/itt_tsquash.prla
+1 -1 metaprl/theories/itt/itt_tunion.ml
+2 -2 metaprl/theories/itt/itt_tunion.prla
+1 -1 metaprl/theories/itt/itt_union.ml
+2 -2 metaprl/theories/itt/itt_union.prla
+2 -2 metaprl/theories/itt/itt_union2.ml
+1 -1 metaprl/theories/itt/itt_unit.ml
+2 -2 metaprl/theories/itt/itt_unit.prla
+2 -2 metaprl/theories/itt/itt_void.ml
+2 -2 metaprl/theories/itt/itt_void.prla
+1 -1 metaprl/theories/itt/itt_w.ml
+2 -2 metaprl/theories/itt/itt_w.prla
+1 -1 metaprl/theories/itt/itt_well_founded.ml
+2 -2 metaprl/theories/itt/itt_well_founded.prla
+2 -2 metaprl/theories/sil/sil_itt_sos.ml
+1 -1 metaprl/theories/sil/sil_itt_state_types.ml
+1 -1 metaprl/theories/sil/sil_sos.ml.new
+1 -1 metaprl/theories/sil/sil_state_model.ml
+2 -2 metaprl/theories/tptp/tptp.ml
+2 -2 metaprl/theories/tptp/tptp.prla
+1 -1 metaprl/theories/tptp/tptp_prove.ml