# HG changeset patch
# User nipkow
# Date 1387570141 -3600
# Node ID fac0c76bbda265c9e2527f4e41aa7a4315dcd3a2
# Parent  16511f84913ce3fe3ec3b0a42389dcbd15167632# Parent  327f282799dbbb360b243dc91fcb627b7cea772d
merged

diff -r 16511f84913c -r fac0c76bbda2 src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Fri Dec 20 20:36:38 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Fri Dec 20 21:09:01 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
 
diff -r 16511f84913c -r fac0c76bbda2 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Fri Dec 20 20:36:38 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Fri Dec 20 21:09:01 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