--- a/doc-src/Ref/ref.tex Fri Apr 15 16:53:01 1994 +0200
+++ b/doc-src/Ref/ref.tex Fri Apr 15 17:16:23 1994 +0200
@@ -32,7 +32,7 @@
\begin{document}
\index{definitions|see{rewriting, meta-level}}
\index{rewriting!object-level|see{simplification}}
-\index{rules!meta-level|see{meta-rules}}
+\index{meta-rules|see{meta-rules}}
\maketitle
\pagenumbering{roman} \tableofcontents \clearfirst
@@ -43,12 +43,14 @@
\include{tctical}
\include{thm}
\include{theories}
+\include{defining}
+\include{syntax}
\include{substitution}
\include{simplifier}
\include{classical}
%%seealso's must be last so that they appear last in the index entries
-\index{rewriting!meta-level|seealso{tactics, theorems}}
+\index{meta-rewriting|seealso{tactics, theorems}}
\begingroup
\bibliographystyle{plain} \small\raggedright\frenchspacing