--- a/doc-src/IsarRef/Thy/document/Synopsis.tex Mon Dec 12 17:22:48 2011 +0100
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex Mon Dec 12 19:47:50 2011 +0100
@@ -691,7 +691,7 @@
\ \ \isacommand{also}\isamarkupfalse%
\isanewline
\ \ \isacommand{have}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}b{\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}b\ {\isaliteral{5C3C6C653E}{\isasymle}}\ c{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
\isanewline
\ \ \isacommand{also}\isamarkupfalse%
\isanewline
@@ -722,7 +722,7 @@
\item The notion of \isa{trans} rule is very general due to the
flexibility of Isabelle/Pure rule composition.
- \item User applications may declare there own rules, with some care
+ \item User applications may declare their own rules, with some care
about the operational details of higher-order unification.
\end{itemize}%