added proof state output warning
Thu, 12 Nov 2015 11:05:38 +0100
changeset 61643 712d3d64c38b
parent 61642 40ca618e1b2d
child 61644 b1c24adc1581
added proof state output warning
--- 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}
+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.