Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-06-11 16:22:04 -0700 (Tue, 11 Jun 2002)
Revision: 3712
Log message:

      theories.pdf reorganization - now each major theory (Base, Itt, Czf and Mc)
      has its own chapter.
      
      For consistensy, I've renamed the documentation therms for headings.
      The current terms are:
      - @theory{'t} - for chapter headings to use in xxx_theory modules (which should go first in
      theory printouts).
      - @module[name] - for module (LaTeX \section) heading
      - @modsection[name] - for a heading of a module section (LaTeX \subsectipon).
      - @modsubsection[name] - for a heading of a module subsection (LaTex \subsubsection)
      
      Also, what used to be hreftheory and reftheory are now called hrefmodule and refmodule.
      I have not implemented the new [h]reftheory yet.
      

Changes  Path
+0 -1 metaprl/doc/latex/theories/Makefile
+11 -5 metaprl/doc/latex/theories/all-theories.tex
+1 -1 metaprl/doc/latex/theories/itt/print.ml
+1 -1 metaprl/theories/base/base_auto_tactic.ml
+2 -2 metaprl/theories/base/base_dtactic.ml
+2 -2 metaprl/theories/base/base_rewrite.ml
+15 -14 metaprl/theories/base/base_theory.mlz
+1 -1 metaprl/theories/base/base_trivial.ml
+1 -1 metaprl/theories/base/typeinf.ml
+3 -3 metaprl/theories/czf/czf_itt_abel_group.ml
+5 -5 metaprl/theories/czf/czf_itt_axioms.ml
+5 -5 metaprl/theories/czf/czf_itt_coset.ml
+4 -4 metaprl/theories/czf/czf_itt_cyclic_group.ml
+4 -4 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+6 -6 metaprl/theories/czf/czf_itt_dall.ml
+6 -6 metaprl/theories/czf/czf_itt_dexists.ml
+1 -1 metaprl/theories/czf/czf_itt_empty.ml
+7 -7 metaprl/theories/czf/czf_itt_eq.ml
+8 -8 metaprl/theories/czf/czf_itt_equiv.ml
+3 -3 metaprl/theories/czf/czf_itt_fol.mlz
+9 -9 metaprl/theories/czf/czf_itt_group.ml
+4 -4 metaprl/theories/czf/czf_itt_group_bvd.ml
+5 -5 metaprl/theories/czf/czf_itt_group_power.ml
+6 -6 metaprl/theories/czf/czf_itt_hom.ml
+4 -4 metaprl/theories/czf/czf_itt_inv_image.ml
+6 -6 metaprl/theories/czf/czf_itt_isect.ml
+3 -3 metaprl/theories/czf/czf_itt_iso.ml
+4 -4 metaprl/theories/czf/czf_itt_ker.ml
+4 -4 metaprl/theories/czf/czf_itt_kleingroup.ml
+4 -4 metaprl/theories/czf/czf_itt_member.ml
+6 -6 metaprl/theories/czf/czf_itt_nat.ml
+4 -4 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+5 -5 metaprl/theories/czf/czf_itt_pair.ml
+3 -3 metaprl/theories/czf/czf_itt_power.ml
+1 -1 metaprl/theories/czf/czf_itt_rel.ml
+5 -5 metaprl/theories/czf/czf_itt_sall.ml
+7 -7 metaprl/theories/czf/czf_itt_sep.ml
+7 -7 metaprl/theories/czf/czf_itt_set.ml
+5 -5 metaprl/theories/czf/czf_itt_set_bvd.ml
+5 -5 metaprl/theories/czf/czf_itt_setdiff.ml
+5 -5 metaprl/theories/czf/czf_itt_sexists.ml
+5 -5 metaprl/theories/czf/czf_itt_singleton.ml
+5 -5 metaprl/theories/czf/czf_itt_subgroup.ml
+5 -5 metaprl/theories/czf/czf_itt_subset.ml
+28 -26 metaprl/theories/czf/czf_itt_theory.mlz
+5 -5 metaprl/theories/czf/czf_itt_union.ml
+5 -5 metaprl/theories/itt/itt_atom.ml
+7 -7 metaprl/theories/itt/itt_bisect.ml
+17 -17 metaprl/theories/itt/itt_bool.ml
+4 -4 metaprl/theories/itt/itt_bunion.ml
+4 -4 metaprl/theories/itt/itt_collection.ml
+1 -1 metaprl/theories/itt/itt_comment.ml
+2 -2 metaprl/theories/itt/itt_decidable.ml
+10 -10 metaprl/theories/itt/itt_dfun.ml
+9 -9 metaprl/theories/itt/itt_disect.ml
+10 -10 metaprl/theories/itt/itt_dprod.ml
+8 -8 metaprl/theories/itt/itt_equal.ml
+6 -6 metaprl/theories/itt/itt_esquash.ml
+1 -1 metaprl/theories/itt/itt_eta.ml
+9 -9 metaprl/theories/itt/itt_fun.ml
+1 -1 metaprl/theories/itt/itt_int_arith.ml
+12 -12 metaprl/theories/itt/itt_int_base.ml
+8 -10 metaprl/theories/itt/itt_int_ext.ml
+6 -6 metaprl/theories/itt/itt_isect.ml
+10 -10 metaprl/theories/itt/itt_list.ml
+3 -3 metaprl/theories/itt/itt_list2.ml
+12 -12 metaprl/theories/itt/itt_logic.ml
+1 -1 metaprl/theories/itt/itt_nat.ml
+5 -5 metaprl/theories/itt/itt_prec.ml
+7 -7 metaprl/theories/itt/itt_prod.ml
+5 -5 metaprl/theories/itt/itt_quotient.ml
+5 -5 metaprl/theories/itt/itt_record.ml
+1 -1 metaprl/theories/itt/itt_record_exm.ml
+12 -12 metaprl/theories/itt/itt_rfun.ml
+7 -7 metaprl/theories/itt/itt_set.ml
+7 -7 metaprl/theories/itt/itt_squash.ml
+5 -5 metaprl/theories/itt/itt_squiggle.ml
+6 -6 metaprl/theories/itt/itt_srec.ml
+12 -12 metaprl/theories/itt/itt_struct.ml
+6 -6 metaprl/theories/itt/itt_struct2.ml
+5 -5 metaprl/theories/itt/itt_subtype.ml
+2 -1 metaprl/theories/itt/itt_theory.ml
+5 -5 metaprl/theories/itt/itt_tunion.ml
+8 -8 metaprl/theories/itt/itt_union.ml
+8 -8 metaprl/theories/itt/itt_unit.ml
+4 -4 metaprl/theories/itt/itt_void.ml
+6 -6 metaprl/theories/itt/itt_w.ml
+4 -4 metaprl/theories/itt/itt_well_founded.ml
+1 -1 metaprl/theories/mc/mp_mc_const_elim.ml
+1 -1 metaprl/theories/mc/mp_mc_deadcode.ml
+4 -4 metaprl/theories/mc/mp_mc_fir_base.ml
+1 -1 metaprl/theories/mc/mp_mc_fir_eval.ml
+10 -10 metaprl/theories/mc/mp_mc_fir_exp.ml
+1 -1 metaprl/theories/mc/mp_mc_fir_phobos.ml
+1 -1 metaprl/theories/mc/mp_mc_fir_prog.ml
+4 -4 metaprl/theories/mc/mp_mc_fir_ty.ml
+1 -1 metaprl/theories/mc/mp_mc_inline.ml
+1 -1 metaprl/theories/mc/mp_mc_inline_aux.ml
+2 -1 metaprl/theories/mc/mp_mc_theory.mlz
+2 -2 metaprl/theories/tactic/base_dform.ml
+41 -40 metaprl/theories/tactic/comment.ml
+11 -10 metaprl/theories/tactic/comment.mli
+1 -1 metaprl/theories/tactic/mptop.ml
+2 -2 metaprl/theories/tactic/nuprl_font.ml
+2 -2 metaprl/theories/tactic/perv.ml
+1 -1 metaprl/theories/tactic/summary.ml
+12 -12 metaprl/theories/tactic/top_conversionals.ml
+7 -7 metaprl/theories/tactic/top_tacticals.ml
+2 -2 metaprl/theories/tactic/var.ml
+8 -7 texinputs/metaprl.tex
Deleted texinputs/section-hack.sty