/[mojave]/texinputs/metaprl.tex
ViewVC logotype

Log of /texinputs/metaprl.tex

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (as text) (annotate)
Sticky Revision:

Revision 3591 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 3816 byte(s)
Diff to previous 3584
- Added an option to be have "THEORIES=all" in mk/config
(instead of THEORIES="long list of theories").
I will change all my nightly scripts to use THEORIES=all.

- Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
that would automatically contain \inputs corresponding to TEXTHEORIES.
(Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
was changed).

- Minor fixes in some display forms.

- Removed theories/caml that never had anything useful.

- Removed a few files from theories/ocaml_doc that seemed to be there by accident
(Jason, can you confirm?).


Revision 3584 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 1 month ago) by nogin
File length: 3773 byte(s)
Diff to previous 3254
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.


Revision 3254 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Thu Jun 7 19:14:04 2001 UTC (20 years ago) by nogin
File length: 3745 byte(s)
Diff to previous 3235
- For symbolic keywords, use tt instead of bf
- Use tt for non-math < and > to make sure that are displayed properly.


Revision 3235 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Sun May 20 23:04:08 2001 UTC (20 years, 1 month ago) by nogin
File length: 3637 byte(s)
Diff to previous 3232
Display form fixes.

- TeX: all object-level terms (theorem statements, etc) are now typeset
in math mode.

- Tex: variable names are now parsed to detect indeces. In particular,
  'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}.

- Tex: `|' symbol in display forms is now always handled correctly.

- Numerous small fixes.


Revision 3232 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Thu May 17 22:06:20 2001 UTC (20 years, 1 month ago) by nogin
File length: 3569 byte(s)
Diff to previous 3226
I joined Itt_hide and Itt_squash into a single theory - Itt_squash that deals
with both the meta-level squash operator (Base_trivial!squash{}) and the type
theory squash operator (Itt_squash!squash{'A}). This makes sense because
these two operators are almost exectly the same in nature except for oe
being a meta-level operator and another - an object-level one.

This commit also renames Itt_hide!hide into Itt_squash!squash. This means
that we now have two operators named "squash", however this should not cause
any confusion since all part of the system (including the parser and display
form mechanism) take into account the number of arguments.

Warning: This commit probably broke lots of proofs. I plan to fix that
after I have a chance to rewrite the squash theory a little better (for
now I just copied the one from Itt_hide). Hopefully, I should have it
done within a week.


Revision 3226 - (view) (download) (as text) (annotate) - [select for diffs]
Modified Wed May 9 16:26:54 2001 UTC (20 years, 1 month ago) by nogin
File length: 3505 byte(s)
Diff to previous 3057
- Removed references to [un]fold_momber from FOL.
- TeX fixes.


Revision 3057 - (view) (download) (as text) (annotate) - [select for diffs]
Added Sun Sep 10 18:26:37 2000 UTC (20 years, 9 months ago) by jyh
File length: 3502 byte(s)
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]
   arg
   @end[opname]

   Text sequences count as a single term.  So, for instance, the
   term @bf{Hello world} display the "Hello world" text in a bold
   font.

   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/comment.ml 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
   directory.

   For example, we could either do this:

   @begin[spelling]
   Aleksey Nogin
   @end[spelling]

   Or we could just add Alexey to either $cwd/.ispell_english, or
   ~/.ispell_english.

   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.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26