# HG changeset patch
# User nipkow
# Date 1350046676 -7200
# Node ID 007f03af6c6a6d387a57664bd18451494102f161
# Parent  2af09163cba18ed8a8b7acdb1b53046b39d8e7f2
tuned

diff -r 2af09163cba1 -r 007f03af6c6a src/Doc/ProgProve/Isar.thy
--- 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)\""}\\