30 \binperiod %%%treat . like a binary operator |
30 \binperiod %%%treat . like a binary operator |
31 |
31 |
32 \begin{document} |
32 \begin{document} |
33 \index{definitions|see{rewriting, meta-level}} |
33 \index{definitions|see{rewriting, meta-level}} |
34 \index{rewriting!object-level|see{simplification}} |
34 \index{rewriting!object-level|see{simplification}} |
35 \index{rules!meta-level|see{meta-rules}} |
35 \index{meta-rules|see{meta-rules}} |
36 |
36 |
37 \maketitle |
37 \maketitle |
38 \pagenumbering{roman} \tableofcontents \clearfirst |
38 \pagenumbering{roman} \tableofcontents \clearfirst |
39 |
39 |
40 \include{introduction} |
40 \include{introduction} |
41 \include{goals} |
41 \include{goals} |
42 \include{tactic} |
42 \include{tactic} |
43 \include{tctical} |
43 \include{tctical} |
44 \include{thm} |
44 \include{thm} |
45 \include{theories} |
45 \include{theories} |
|
46 \include{defining} |
|
47 \include{syntax} |
46 \include{substitution} |
48 \include{substitution} |
47 \include{simplifier} |
49 \include{simplifier} |
48 \include{classical} |
50 \include{classical} |
49 |
51 |
50 %%seealso's must be last so that they appear last in the index entries |
52 %%seealso's must be last so that they appear last in the index entries |
51 \index{rewriting!meta-level|seealso{tactics, theorems}} |
53 \index{meta-rewriting|seealso{tactics, theorems}} |
52 |
54 |
53 \begingroup |
55 \begingroup |
54 \bibliographystyle{plain} \small\raggedright\frenchspacing |
56 \bibliographystyle{plain} \small\raggedright\frenchspacing |
55 \bibliography{atp,funprog,general,logicprog,theory} |
57 \bibliography{atp,funprog,general,logicprog,theory} |
56 \endgroup |
58 \endgroup |