Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-01 21:54:27 -0700 (Thu, 01 May 2003)
Revision: 4540
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
      

Changes	Path
+1 -1	metaprl/doc/htmlman/tutorial/mp-all.html
+1 -1	metaprl/doc/htmlman/tutorial/mp-base-auto.html
+0 -1	metaprl/doc/htmlman/user-guide/mp-editor.html
+13 -12	metaprl/doc/itt_quickref.txt
+3 -3	metaprl/doc/latex/theories/base/print.ml
+2 -2	metaprl/editor/ml/tests/czf.ml
+2 -2	metaprl/editor/ml/tests/prop-pigeon.ml
+2 -2	metaprl/editor/ml/tutorial.ml
+4 -4	metaprl/editor/ml/tutorial_itt.ml
+2 -2	metaprl/editor/ml/x.ml
+4 -4	metaprl/library/mbs-mpl.txt
+4 -0	metaprl/support/tactics/Makefile
Added	metaprl/support/tactics/auto_tactic.ml
Properties	metaprl/support/tactics/auto_tactic.ml
Added	metaprl/support/tactics/auto_tactic.mli
Properties	metaprl/support/tactics/auto_tactic.mli
Added	metaprl/support/tactics/base_cache.ml
Properties	metaprl/support/tactics/base_cache.ml
Added	metaprl/support/tactics/base_cache.mli
Properties	metaprl/support/tactics/base_cache.mli
Added	metaprl/support/tactics/dtactic.ml
Properties	metaprl/support/tactics/dtactic.ml
Added	metaprl/support/tactics/dtactic.mli
Properties	metaprl/support/tactics/dtactic.mli
Added	metaprl/support/tactics/typeinf.ml
Properties	metaprl/support/tactics/typeinf.ml
Added	metaprl/support/tactics/typeinf.mli
Properties	metaprl/support/tactics/typeinf.mli
+0 -4	metaprl/theories/base/Makefile
Deleted	metaprl/theories/base/base_auto_tactic.ml
Deleted	metaprl/theories/base/base_auto_tactic.mli
Deleted	metaprl/theories/base/base_cache.ml
Deleted	metaprl/theories/base/base_cache.mli
Deleted	metaprl/theories/base/base_dtactic.ml
Deleted	metaprl/theories/base/base_dtactic.mli
+2 -2	metaprl/theories/base/base_rewrite.ml
+1 -1	metaprl/theories/base/base_rewrite.mli
+1 -1	metaprl/theories/base/base_rewrite.prla
+6 -6	metaprl/theories/base/base_theory.mlz
Deleted	metaprl/theories/base/typeinf.ml
Deleted	metaprl/theories/base/typeinf.mli
+2 -2	metaprl/theories/czf/czf_itt_abel_group.ml
+2 -2	metaprl/theories/czf/czf_itt_abel_group.mli
+2 -2	metaprl/theories/czf/czf_itt_abel_group.prla
+2 -2	metaprl/theories/czf/czf_itt_all.ml
+2 -2	metaprl/theories/czf/czf_itt_all.prla
+1 -1	metaprl/theories/czf/czf_itt_and.ml
+2 -2	metaprl/theories/czf/czf_itt_and.prla
+2 -2	metaprl/theories/czf/czf_itt_axioms.prla
+2 -2	metaprl/theories/czf/czf_itt_bool.ml
+2 -2	metaprl/theories/czf/czf_itt_bool.prla
+2 -2	metaprl/theories/czf/czf_itt_comment.prla
+2 -2	metaprl/theories/czf/czf_itt_coset.ml
+2 -2	metaprl/theories/czf/czf_itt_coset.mli
+2 -2	metaprl/theories/czf/czf_itt_coset.prla
+2 -2	metaprl/theories/czf/czf_itt_cyclic_group.ml
+2 -2	metaprl/theories/czf/czf_itt_cyclic_group.mli
+2 -2	metaprl/theories/czf/czf_itt_cyclic_group.prla
+2 -2	metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+2 -2	metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+2 -2	metaprl/theories/czf/czf_itt_cyclic_subgroup.prla
+1 -1	metaprl/theories/czf/czf_itt_dall.ml
+2 -2	metaprl/theories/czf/czf_itt_dall.prla
+1 -1	metaprl/theories/czf/czf_itt_dexists.ml
+2 -2	metaprl/theories/czf/czf_itt_dexists.prla
+1 -1	metaprl/theories/czf/czf_itt_empty.ml
+2 -2	metaprl/theories/czf/czf_itt_empty.prla
+2 -2	metaprl/theories/czf/czf_itt_eq.ml
+2 -2	metaprl/theories/czf/czf_itt_eq.prla
+2 -2	metaprl/theories/czf/czf_itt_equiv.ml
+2 -2	metaprl/theories/czf/czf_itt_equiv.mli
+2 -2	metaprl/theories/czf/czf_itt_equiv.prla
+2 -2	metaprl/theories/czf/czf_itt_exists.ml
+2 -2	metaprl/theories/czf/czf_itt_exists.prla
+1 -1	metaprl/theories/czf/czf_itt_false.ml
+2 -2	metaprl/theories/czf/czf_itt_false.prla
+2 -2	metaprl/theories/czf/czf_itt_group.ml
+2 -2	metaprl/theories/czf/czf_itt_group.mli
+2 -2	metaprl/theories/czf/czf_itt_group.prla
+2 -2	metaprl/theories/czf/czf_itt_group_bvd.ml
+2 -2	metaprl/theories/czf/czf_itt_group_bvd.mli
+2 -2	metaprl/theories/czf/czf_itt_group_bvd.prla
+2 -2	metaprl/theories/czf/czf_itt_group_power.ml
+2 -2	metaprl/theories/czf/czf_itt_group_power.mli
+2 -2	metaprl/theories/czf/czf_itt_group_power.prla
+2 -2	metaprl/theories/czf/czf_itt_hom.ml
+2 -2	metaprl/theories/czf/czf_itt_hom.mli
+2 -2	metaprl/theories/czf/czf_itt_hom.prla
+1 -1	metaprl/theories/czf/czf_itt_implies.ml
+2 -2	metaprl/theories/czf/czf_itt_implies.prla
+2 -2	metaprl/theories/czf/czf_itt_infinity.prla
+2 -2	metaprl/theories/czf/czf_itt_inv_image.ml
+2 -2	metaprl/theories/czf/czf_itt_inv_image.mli
+2 -2	metaprl/theories/czf/czf_itt_inv_image.prla
+1 -1	metaprl/theories/czf/czf_itt_isect.ml
+2 -2	metaprl/theories/czf/czf_itt_isect.prla
+2 -2	metaprl/theories/czf/czf_itt_iso.ml
+2 -2	metaprl/theories/czf/czf_itt_iso.mli
+2 -2	metaprl/theories/czf/czf_itt_iso.prla
+2 -2	metaprl/theories/czf/czf_itt_ker.ml
+2 -2	metaprl/theories/czf/czf_itt_ker.mli
+2 -2	metaprl/theories/czf/czf_itt_ker.prla
+2 -2	metaprl/theories/czf/czf_itt_kleingroup.ml
+2 -2	metaprl/theories/czf/czf_itt_kleingroup.mli
+2 -2	metaprl/theories/czf/czf_itt_kleingroup.prla
+1 -1	metaprl/theories/czf/czf_itt_member.ml
+2 -2	metaprl/theories/czf/czf_itt_member.prla
+1 -1	metaprl/theories/czf/czf_itt_nat.ml