/[mojave]/metaprl/theories/czf/czf_itt_axioms.ml
ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_axioms.ml

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 1 month ago) by nogin
File length: 5310 byte(s)
Diff to previous 3057
- 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 3057 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 18:26:37 2000 UTC (20 years, 9 months ago) by jyh
File length: 5309 byte(s)
Diff to previous 3052
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.


Revision 3052 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 30 00:56:48 2000 UTC (20 years, 9 months ago) by jyh
File length: 3943 byte(s)
Diff to previous 2822
Two changes.
   1. expand () now does sloppy expansion, so that proofs
      can be replayed even if the goal of a proof has changed.
      This also means that proof copy/paste should work.

   2. I fixed up CZF.  This is a pretty cool set theory, where
      we get the usual ZF axioms (except excluded middle).  The
      normal things like numbers can be coded in the usual
      way, except we get decidability of number equality and
      other constructive ideas.  Reals can be coded with
      Dedekind cuts according to Aczel.  This theory is the
      basic set theory with just the axioms.  Before going on,
      it is probably a good idea to stratify the sets with
      levels, so we can formalize the notion of classes.


Revision 2822 - (view) (download) (annotate) - [select for diffs]
Modified Fri Oct 22 01:07:59 1999 UTC (21 years, 8 months ago) by nogin
File length: 3666 byte(s)
Diff to previous 2494
Added new function to mp_debug
let show_loading s = if !debug_load then Printf.eprintf s eflush

and replaced all usages of debug_load with show_loading


Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 3694 byte(s)
Diff to previous 2456
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.


Revision 2456 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 5 22:31:37 1998 UTC (22 years, 9 months ago) by jyh
File length: 3698 byte(s)
Diff to previous 2336
Added license headers to each of the files in preparation for
the first major release.  The license is GNU public license; if
any of you have problems with that, let me know right away.  When
you add new code, you should credit yourself as the author.  When
you modify code, you should add a "Modified by:" to the header,
and possibly a short summary of your changes.

I tried to get the Author lists as correct as I remember, but there
are more than 550 files(!) and I may have made some mistakes. Please
add yourself if I didn't do it right.


Revision 2336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 21 22:47:13 1998 UTC (22 years, 11 months ago) by jyh
File length: 2539 byte(s)
Diff to previous 2333
Added NL toploop so that we can compile NL native code.


Revision 2333 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 17 15:39:32 1998 UTC (22 years, 11 months ago) by jyh
File length: 2612 byte(s)
Diff to previous 2320
CZF is complete, although we may wish to add pairing and inf.


Revision 2320 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 9 21:08:59 1998 UTC (22 years, 11 months ago) by jyh
File length: 1726 byte(s)
Diff to previous 2307
Upgraded czf.


Revision 2307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 17:55:31 1998 UTC (22 years, 11 months ago) by nogin
File length: 1646 byte(s)
Diff to previous 2272
Removed $Log messages from all NL files.


Revision 2272 - (view) (download) (annotate) - [select for diffs]
Added Tue Jun 23 22:12:44 1998 UTC (23 years ago) by jyh
File length: 1762 byte(s)
Improved rewriter speed with conversion tree and flist.


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