/[mojave]/metaprl/doc/latex/theories/base/print.ml
ViewVC logotype

Contents of /metaprl/doc/latex/theories/base/print.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3584 - (show annotations) (download)
Thu Apr 25 15:28:40 2002 UTC (19 years, 3 months ago) by nogin
File size: 1323 byte(s)
- 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.

1 (*
2 *
3 * ----------------------------------------------------------------
4 *
5 * Copyright (C) 2000 Jason Hickey, Caltech
6 *
7 * This program is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
11 *
12 * This program is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
16 *
17 * You should have received a copy of the GNU General Public License
18 * along with this program; if not, write to the Free Software
19 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
20 *
21 * Author: Jason Hickey
22 * jyh@cs.caltech.edu
23 *)
24
25 set_tex_file "../../doc/latex/theories/base/theory.tex";;
26
27 print_theory "base_theory";;
28 print_theory "summary";;
29 print_theory "mptop";;
30 print_theory "var";;
31 print_theory "top_tacticals";;
32 print_theory "top_conversionals";;
33 print_theory "base_trivial";;
34 print_theory "base_auto_tactic";;
35 print_theory "base_dtactic";;
36 print_theory "base_rewrite";;
37 print_theory "comment";;
38
39 (*
40 * -*-
41 * Local Variables:
42 * Caml-master: "compile"
43 * End:
44 * -*-
45 *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26