--- 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