--- a/doc-src/IsarOverview/Isar/document/Logic.tex Sat Mar 21 12:37:13 2009 +0100
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex Sun Mar 22 19:36:04 2009 +0100
@@ -93,8 +93,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Single-identifier formulae such as \isa{A} need not
-be enclosed in double quotes. However, we will continue to do so for
+\noindent As you see above, single-identifier formulae such as \isa{A}
+need not be enclosed in double quotes. However, we will continue to do so for
uniformity.
Instead of applying fact \isa{a} via the \isa{rule} method, we can