doc-src/TutorialI/Misc/document/def_rewr.tex

--- a/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 15:43:29 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/def_rewr.tex	Tue Aug 29 16:05:13 2000 +0200
@@ -26,9 +26,9 @@
 \begin{isamarkuptxt}%
 \noindent
 In this particular case, the resulting goal
-\begin{isabellepar}%
+\begin{isabelle}
 ~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
-\end{isabellepar}%
+\end{isabelle}
 can be proved by simplification. Thus we could have proved the lemma outright%
 \end{isamarkuptxt}%
 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ exor{\isacharunderscore}def{\isacharparenright}%