diff -r 620db300c038 -r 57753e0ec1d4 doc-src/IsarOverview/Isar/Logic.thy
--- a/doc-src/IsarOverview/Isar/Logic.thy	Sat Mar 21 12:37:13 2009 +0100
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Sun Mar 22 19:36:04 2009 +0100
@@ -30,8 +30,8 @@
   show A by(rule a)
 qed
 
-text{*\noindent Single-identifier formulae such as @{term A} need not
-be enclosed in double quotes. However, we will continue to do so for
+text{*\noindent As you see above, single-identifier formulae such as @{term A}
+need not be enclosed in double quotes. However, we will continue to do so for
 uniformity.
 
 Instead of applying fact @{text a} via the @{text rule} method, we can