# HG changeset patch
# User nipkow
# Date 1447322738 -3600
# Node ID 712d3d64c38b55e6995de5dd73e5de00a690de56
# Parent  40ca618e1b2d349b7b9433d7677e08ee819ee5e6
added proof state output warning

diff -r 40ca618e1b2d -r 712d3d64c38b src/Doc/Prog_Prove/Basics.thy
--- a/src/Doc/Prog_Prove/Basics.thy	Wed Nov 11 19:22:18 2015 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy	Thu Nov 12 11:05:38 2015 +0100
@@ -135,10 +135,18 @@
 \isacommand{begin} and \isacommand{datatype}.  Embedded in this syntax are
 the types and formulas of HOL.  To distinguish the two levels, everything
 HOL-specific (terms and types) must be enclosed in quotation marks:
-\texttt{"}\dots\texttt{"}. To lessen this burden, quotation marks around a
+\texttt{"}\dots\texttt{"}. Quotation marks around a
 single identifier can be dropped.  When Isabelle prints a syntax error
 message, it refers to the HOL syntax as the \concept{inner syntax} and the
 enclosing theory language as the \concept{outer syntax}.
+
+\subsection{Proof State}
+
+\begin{warn}
+By default Isabelle/jEdit not longer shows the current proof state
+in the output window. You should enable this by ticking
+Plugins $>$ Plugin Options $>$ Editor Output State.
+\end{warn}
 *}
 (*<*)
 end