--- a/doc-src/AxClass/generated/Product.tex Thu Aug 31 17:59:59 2000 +0200
+++ b/doc-src/AxClass/generated/Product.tex Fri Sep 01 00:27:41 2000 +0200
@@ -1,4 +1,5 @@
-\begin{isabelle}%
+%
+\begin{isabellebody}%
%
\isamarkupheader{Syntactic classes}
\isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}%
@@ -74,7 +75,7 @@
meta-logic, because there is no internal notion of ``providing
operations'' or even ``names of functions''.%
\end{isamarkuptext}%
-\isacommand{end}\end{isabelle}%
+\isacommand{end}\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"