--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri May 25 18:24:11 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri May 25 18:25:17 2007 +0200
@@ -461,7 +461,7 @@
Note the space between \verb!@! and \verb!{! in the tabular argument.
It prevents Isabelle from interpreting \verb!@ {~~...~~}!
as an antiquotation. The styles \verb!lhs! and \verb!rhs!
- extract the left hand side (or right hand side respectivly) from the
+ extract the left hand side (or right hand side respectively) from the
conclusion of propositions consisting of a binary operator
(e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
@@ -531,7 +531,7 @@
After this \verb!setup!,
there will be a new style available named \verb!my_concl!, thus allowing
- antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
+ antiquotations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
\end{isamarkuptext}%
\isamarkuptrue%