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 
* Camlmaster: "compile" 
43 
* End: 
44 
* * 
45 
*) 