--- a/src/Doc/ProgProve/Isar.thy Fri Oct 12 14:05:30 2012 +0200
+++ b/src/Doc/ProgProve/Isar.thy Fri Oct 12 14:57:56 2012 +0200
@@ -736,8 +736,8 @@
proposition to be proved in each case is not the whole implication but only
its conclusion; the premises of the implication are immediately made
assumptions of that case. That is, if in the above proof we replace
-\isacom{show}~@{text"P(n)"} by
-\mbox{\isacom{show}~@{text"A(n) \<Longrightarrow> P(n)"}}
+\isacom{show}~@{text"\"P(n)\""} by
+\mbox{\isacom{show}~@{text"\"A(n) \<Longrightarrow> P(n)\""}}
then \isacom{case}~@{text 0} stands for
\begin{quote}
\isacom{assume} \ @{text"0: \"A(0)\""}\\