Changes by: Jason Hickey (jyh at
Date: 2000-09-10 11:26:37 -0700 (Sun, 10 Sep 2000)
Revision: 3057
Log message:

      This jumbo update is a documentation update.  There are no
      logical changes.  I did two things:
      1. First, comments that begin with the sequence "(*!" are
         interpreted as structured comments.  The contents are parsed
         as terms, and the comments will display in the editor window.
         The comments may contain arbitrary text, as usual, and they
         can also contain explicit terms.  The syntax for terms is:
         @opname[p1, ..., pn]{t1; ...; tm}
         or there is an alternate syntax:
         @begin[opname, p1, ..., pn]
         Text sequences count as a single term.  So, for instance, the
         term @bf{Hello world} display the "Hello world" text in a bold
         The "doc" term is used for text that is considered to be
         documentation.  There is a set of LaTeX-like terms that you can
         use to produce good-looking documentation.  These are all
         documented in the theories/tactic/ module.  The exact
         syntax of structured comments is defined in the
         mllib/comment_parse.mll file.  You can also look at any of the
         module in the theories/itt directory if you want to see examples.
         You can generate a pritable version of documentation with the
         print_theory command in the editor.  For example, the command
         # print_theory "itt_equal";;
         produces a file called output.tex that can be formatted with
         your favorite version of latex2e.  You can also generate a
         manule of all the theories by running "make tex" in the
         editor/ml directory.  Or you can run "make" in the
         doc/latex/theories directory.
         The files are hyperlinked, and they contain a table of contents
         and an index.  The preferred reader is acrobat, and the preferred
         formatter is pdflatex.
      2. Second, I documented the tactic, base, itt, and czf theories.
      3. Oh, and I also added a spelling checker:)  You can turn on the
         spelling checker with the -debug spell option or MP_DEBUG=spell.
         If prlc thinks that your files contain spelling mistakes, it will
         print them out and abort.  You can fix this problem by 1) fixing
         the spelling error, 2) adding the words withing a @spelling{words}
         term in a comment, or adding the words to you .ispell_english
         For example, we could either do this:
         Aleksey Nogin
         Or we could just add Alexey to either $cwd/.ispell_english, or
         The spell checker uses /usr/dict/words as a database, which it
         compiles to a hashtable in /tmp/metaprl-spell-$USER.dat.  Don't
         worry about the tmp file, it is generated automatically.

Changes  Path
Properties metaprl/doc/latex/theories
Added metaprl/doc/latex/theories/Makefile
Properties metaprl/doc/latex/theories/Makefile
Added metaprl/doc/latex/theories/README
Properties metaprl/doc/latex/theories/README
Added metaprl/doc/latex/theories/all-theories.bbl
Properties metaprl/doc/latex/theories/all-theories.bbl
Added metaprl/doc/latex/theories/all-theories.tex
Properties metaprl/doc/latex/theories/all-theories.tex
Properties metaprl/doc/latex/theories/base
Added metaprl/doc/latex/theories/base/
Properties metaprl/doc/latex/theories/base/
Properties metaprl/doc/latex/theories/czf
Added metaprl/doc/latex/theories/czf/
Properties metaprl/doc/latex/theories/czf/
Properties metaprl/doc/latex/theories/fol
Added metaprl/doc/latex/theories/fol/
Properties metaprl/doc/latex/theories/fol/
Properties metaprl/doc/latex/theories/itt
Added metaprl/doc/latex/theories/itt/
Properties metaprl/doc/latex/theories/itt/
Properties metaprl/doc/ps/theories
Properties metaprl/editor/ml
+15 -0 metaprl/editor/ml/Makefile
+20 -10 metaprl/editor/ml/
+16 -17 metaprl/editor/ml/
+1 -0 metaprl/editor/ml/shell_sig.mlz
+1 -1 metaprl/editor/ml/
Added metaprl/editor/ml/
Properties metaprl/editor/ml/
Added metaprl/editor/ml/shell_tex.mli
Properties metaprl/editor/ml/shell_tex.mli
+2 -1 metaprl/filter/base/Files
+1 -1 metaprl/filter/base/
+7 -1 metaprl/filter/base/
+0 -0 metaprl/filter/base/
+8 -0 metaprl/filter/base/
Added metaprl/filter/base/
Properties metaprl/filter/base/
Added metaprl/filter/base/filter_spell.mli
Properties metaprl/filter/base/filter_spell.mli
+45 -6 metaprl/filter/base/
+4 -0 metaprl/filter/base/filter_summary.mli
+1 -0 metaprl/filter/base/
+1 -0 metaprl/filter/base/
+3 -1 metaprl/filter/filter/
+167 -5 metaprl/filter/filter/
+7 -4 metaprl/filter/filter/filter_parse.mli
Properties metaprl/mllib
+3 -2 metaprl/mllib/Makefile
Added metaprl/mllib/comment_parse.mli
Properties metaprl/mllib/comment_parse.mli
Added metaprl/mllib/comment_parse.mll
Properties metaprl/mllib/comment_parse.mll
+20 -0 metaprl/refiner/reflib/
+120 -33 metaprl/refiner/reflib/
+3 -0 metaprl/refiner/reflib/rformat.mli
+2 -2 metaprl/refiner/reflib/
Added metaprl/theories/base/.ispell_english
Properties metaprl/theories/base/.ispell_english
+0 -2 metaprl/theories/base/Makefile
+74 -5 metaprl/theories/base/
+0 -1 metaprl/theories/base/base_auto_tactic.mli
Deleted metaprl/theories/base/
Deleted metaprl/theories/base/base_dform.mli
+117 -4 metaprl/theories/base/
+64 -4 metaprl/theories/base/
+60 -10 metaprl/theories/base/base_theory.mlz
+19 -4 metaprl/theories/base/
Deleted metaprl/theories/base/
Deleted metaprl/theories/base/summary.mli
+21 -8 metaprl/theories/base/
Properties metaprl/theories/czf
+11 -6 metaprl/theories/czf/Makefile
+12 -16 metaprl/theories/czf/
+0 -17 metaprl/theories/czf/czf_itt_all.mli
+1189 -1518 metaprl/theories/czf/czf_itt_all.prla
+4 -8 metaprl/theories/czf/
+0 -21 metaprl/theories/czf/czf_itt_and.mli
+926 -854 metaprl/theories/czf/czf_itt_and.prla
+60 -22 metaprl/theories/czf/
+4129 -1461 metaprl/theories/czf/czf_itt_axioms.prla
Added metaprl/theories/czf/
Properties metaprl/theories/czf/
Added metaprl/theories/czf/czf_itt_comment.mli
Properties metaprl/theories/czf/czf_itt_comment.mli
Added metaprl/theories/czf/czf_itt_comment.prla
Properties metaprl/theories/czf/czf_itt_comment.prla
+87 -17 metaprl/theories/czf/
+0 -27 metaprl/theories/czf/czf_itt_dall.mli
+5658 -1577 metaprl/theories/czf/czf_itt_dall.prla
+90 -20 metaprl/theories/czf/
+0 -35 metaprl/theories/czf/czf_itt_dexists.mli
+4616 -1567 metaprl/theories/czf/czf_itt_dexists.prla
+31 -6 metaprl/theories/czf/
+0 -13 metaprl/theories/czf/czf_itt_empty.mli
+2482 -517 metaprl/theories/czf/czf_itt_empty.prla
+248 -87 metaprl/theories/czf/
+15 -121 metaprl/theories/czf/czf_itt_eq.mli
+12513 -7664 metaprl/theories/czf/czf_itt_eq.prla
Binary metaprl/theories/czf/czf_itt_eq_inner.prlb
+12 -16 metaprl/theories/czf/
+0 -17 metaprl/theories/czf/czf_itt_exists.mli
+1102 -1777 metaprl/theories/czf/czf_itt_exists.prla
+506 -452 metaprl/theories/czf/czf_itt_false.prla
Added metaprl/theories/czf/czf_itt_fol.mlz
Properties metaprl/theories/czf/czf_itt_fol.mlz
Added metaprl/theories/czf/czf_itt_fol.prla
Properties metaprl/theories/czf/czf_itt_fol.prla
+6 -12 metaprl/theories/czf/
+0 -30 metaprl/theories/czf/czf_itt_implies.mli
+1052 -973 metaprl/theories/czf/czf_itt_implies.prla
Deleted metaprl/theories/czf/
Deleted metaprl/theories/czf/czf_itt_infinity.mli
+420 -370 metaprl/theories/czf/czf_itt_infinity.prla
Added metaprl/theories/czf/
Properties metaprl/theories/czf/
+8 -44 metaprl/theories/czf/czf_itt_isect.mli
Added metaprl/theories/czf/czf_itt_isect.prla
Properties metaprl/theories/czf/czf_itt_isect.prla
+149 -30 metaprl/theories/czf/
+6 -47 metaprl/theories/czf/czf_itt_member.mli
+7280 -4640 metaprl/theories/czf/czf_itt_member.prla
Added metaprl/theories/czf/
Properties metaprl/theories/czf/
Added metaprl/theories/czf/czf_itt_nat.mli
Properties metaprl/theories/czf/czf_itt_nat.mli
Added metaprl/theories/czf/czf_itt_nat.prla
Properties metaprl/theories/czf/czf_itt_nat.prla
+8 -12 metaprl/theories/czf/
+0 -21 metaprl/theories/czf/czf_itt_or.mli
+925 -1352 metaprl/theories/czf/czf_itt_or.prla
Added metaprl/theories/czf/
Properties metaprl/theories/czf/
Added metaprl/theories/czf/czf_itt_pair.mli
Properties metaprl/theories/czf/czf_itt_pair.mli
Added metaprl/theories/czf/czf_itt_pair.prla
Properties metaprl/theories/czf/czf_itt_pair.prla
Added metaprl/theories/czf/
Properties metaprl/theories/czf/
Added metaprl/theories/czf/czf_itt_power.mli
Properties metaprl/theories/czf/czf_itt_power.mli
Added metaprl/theories/czf/czf_itt_power.prla
Properties metaprl/theories/czf/czf_itt_power.prla
Deleted metaprl/theories/czf/czf_itt_pre_theory.mlz
+75 -11 metaprl/theories/czf/
+6 -4 metaprl/theories/czf/czf_itt_rel.mli
Properties texinputs
Added texinputs/metaprl.bib
Properties texinputs/metaprl.bib
Added texinputs/metaprl.tex
Properties texinputs/metaprl.tex