--- a/src/Doc/ProgProve/Isar.thy Fri Dec 20 14:27:07 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy Fri Dec 20 21:08:48 2013 +0100
@@ -116,7 +116,7 @@
If you wonder why @{text 2} directly implies @{text False}: from @{text 2}
it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}.
-\subsection{@{text this}, @{text then}, @{text hence} and @{text thus}}
+\subsection{@{text this}, \isacom{then}, \isacom{hence} and \isacom{thus}}
Labels should be avoided. They interrupt the flow of the reader who has to
scan the context for the point where the label was introduced. Ideally, the
@@ -141,10 +141,10 @@
To compact the text further, Isar has a few convenient abbreviations:
\medskip
-\begin{tabular}{rcl}
-\isacom{then} &=& \isacom{from} @{text this}\\
-\isacom{thus} &=& \isacom{then} \isacom{show}\\
-\isacom{hence} &=& \isacom{then} \isacom{have}
+\begin{tabular}{r@ {\quad=\quad}l}
+\isacom{then} & \isacom{from} @{text this}\\
+\isacom{thus} & \isacom{then} \isacom{show}\\
+\isacom{hence} & \isacom{then} \isacom{have}
\end{tabular}
\medskip
@@ -164,11 +164,11 @@
There are two further linguistic variations:
\medskip
-\begin{tabular}{rcl}
+\begin{tabular}{r@ {\quad=\quad}l}
(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts}
-&=&
+&
\isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\
-\isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this}
+\isacom{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this}
\end{tabular}
\medskip
--- a/src/Doc/ProgProve/Logic.thy Fri Dec 20 14:27:07 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy Fri Dec 20 21:08:48 2013 +0100
@@ -335,7 +335,7 @@
@{text "?x"}. We can see this clearly in rule @{thm[source] conjI}.
These unknowns can later be instantiated explicitly or implicitly:
\begin{itemize}
-\item By hand, using @{text of}.
+\item By hand, using \concept{@{text of}}.
The expression @{text"conjI[of \"a=b\" \"False\"]"}
instantiates the unknowns in @{thm[source] conjI} from left to right with the
two formulas @{text"a=b"} and @{text False}, yielding the rule
@@ -352,8 +352,8 @@
\end{itemize}
We need not instantiate all unknowns. If we want to skip a particular one we
can just write @{text"_"} instead, for example @{text "conjI[of _ \"False\"]"}.
-Unknowns can also be instantiated by name, for example
-@{text "conjI[where ?P = \"a=b\" and ?Q = \"False\"]"}.
+Unknowns can also be instantiated by name using \concept{@{text "where"}}, for example
+@{text "conjI[where ?P = \"a=b\""} \isacom{and} @{text"?Q = \"False\"]"}.
\subsection{Rule Application}
@@ -437,8 +437,8 @@
Forward proof means deriving new theorems from old theorems. We have already
seen a very simple form of forward proof: the @{text of} operator for
-instantiating unknowns in a theorem. The big brother of @{text of} is @{text
-OF} for applying one theorem to others. Given a theorem @{prop"A \<Longrightarrow> B"} called
+instantiating unknowns in a theorem. The big brother of @{text of} is
+\concept{@{text OF}} for applying one theorem to others. Given a theorem @{prop"A \<Longrightarrow> B"} called
@{text r} and a theorem @{text A'} called @{text r'}, the theorem @{text
"r[OF r']"} is the result of applying @{text r} to @{text r'}, where @{text
r} should be viewed as a function taking a theorem @{text A} and returning