--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Mon Oct 12 21:42:14 2015 +0200
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Mon Oct 12 22:03:24 2015 +0200
@@ -231,7 +231,8 @@
``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with
the original axiomatization of @{thm disjE}.
- \medskip We continue propositional logic by introducing absurdity
+ \<^medskip>
+ We continue propositional logic by introducing absurdity
with its characteristic elimination. Plain truth may then be
defined as a proposition that is trivially true.
\<close>
@@ -248,8 +249,8 @@
unfolding true_def ..
text \<open>
- \medskip Now negation represents an implication towards
- absurdity:
+ \<^medskip>
+ Now negation represents an implication towards absurdity:
\<close>
definition
@@ -374,7 +375,7 @@
can now be summarized as follows, using the native Isar statement
format of \secref{sec:framework-stmt}.
- \medskip
+ \<^medskip>
\begin{tabular}{l}
@{text "impI: \<ASSUMES> A \<Longrightarrow> B \<SHOWS> A \<longrightarrow> B"} \\
@{text "impD: \<ASSUMES> A \<longrightarrow> B \<AND> A \<SHOWS> B"} \\[1ex]
@@ -398,7 +399,7 @@
@{text "exI: \<ASSUMES> B a \<SHOWS> \<exists>x. B x"} \\
@{text "exE: \<ASSUMES> \<exists>x. B x \<OBTAINS> a \<WHERE> B a"}
\end{tabular}
- \medskip
+ \<^medskip>
This essentially provides a declarative reading of Pure
rules as Isar reasoning patterns: the rule statements tells how a
@@ -511,7 +512,8 @@
(*>*)
text \<open>
- \bigskip Of course, these proofs are merely examples. As
+ \<^bigskip>
+ Of course, these proofs are merely examples. As
sketched in \secref{sec:framework-subproof}, there is a fair amount
of flexibility in expressing Pure deductions in Isar. Here the user
is asked to express himself adequately, aiming at proof texts of