--- a/src/Doc/Prog_Prove/Basics.thy Mon Mar 29 12:26:13 2021 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy Tue Mar 30 09:42:25 2021 +0200
@@ -132,7 +132,7 @@
\subsection{Quotation Marks}
The textual definition of a theory follows a fixed syntax with keywords like
-\isacommand{begin} and \isacommand{datatype}. Embedded in this syntax are
+\isacom{begin} and \isacom{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{"}. Quotation marks around a
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Mon Mar 29 12:26:13 2021 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Tue Mar 30 09:42:25 2021 +0200
@@ -186,7 +186,7 @@
text\<open>By default, variables \<open>xs\<close>, \<open>ys\<close> and \<open>zs\<close> are of
\<open>list\<close> type.
-Command \indexed{\isacommand{value}}{value} evaluates a term. For example,\<close>
+Command \indexed{\isacom{value}}{value} evaluates a term. For example,\<close>
value "rev(Cons True (Cons False Nil))"
--- a/src/Doc/Prog_Prove/Isar.thy Mon Mar 29 12:26:13 2021 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy Tue Mar 30 09:42:25 2021 +0200
@@ -445,11 +445,11 @@
\begin{samepage}
\begin{quote}
-\isakeyword{have} \<open>"t\<^sub>1 = t\<^sub>2"\<close> \isasymproof\\
-\isakeyword{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
+\isacom{have} \<open>"t\<^sub>1 = t\<^sub>2"\<close> \isasymproof\\
+\isacom{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
\quad $\vdots$\\
-\isakeyword{also have} \<open>"... = t\<^sub>n"\<close> \isasymproof \\
-\isakeyword{finally show} \<open>"t\<^sub>1 = t\<^sub>n"\<close>\ \texttt{.}
+\isacom{also have} \<open>"... = t\<^sub>n"\<close> \isasymproof \\
+\isacom{finally show} \<open>"t\<^sub>1 = t\<^sub>n"\<close>\ \texttt{.}
\end{quote}
\end{samepage}
@@ -461,21 +461,21 @@
In general, if \<open>this\<close> is the theorem \<^term>\<open>p t\<^sub>1 t\<^sub>2\<close> then ``\<open>...\<close>''
stands for \<open>t\<^sub>2\<close>.
\item[``\<open>.\<close>''] (a single dot) is a proof method that solves a goal by one of the
-assumptions. This works here because the result of \isakeyword{finally}
+assumptions. This works here because the result of \isacom{finally}
is the theorem \mbox{\<open>t\<^sub>1 = t\<^sub>n\<close>},
-\isakeyword{show} \<open>"t\<^sub>1 = t\<^sub>n"\<close> states the theorem explicitly,
-and ``\<open>.\<close>'' proves the theorem with the result of \isakeyword{finally}.
+\isacom{show} \<open>"t\<^sub>1 = t\<^sub>n"\<close> states the theorem explicitly,
+and ``\<open>.\<close>'' proves the theorem with the result of \isacom{finally}.
\end{description}
The above proof template also works for arbitrary mixtures of \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close>,
for example:
\begin{quote}
-\isakeyword{have} \<open>"t\<^sub>1 < t\<^sub>2"\<close> \isasymproof\\
-\isakeyword{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
+\isacom{have} \<open>"t\<^sub>1 < t\<^sub>2"\<close> \isasymproof\\
+\isacom{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
\quad $\vdots$\\
-\isakeyword{also have} \<open>"... \<le> t\<^sub>n"\<close> \isasymproof \\
-\isakeyword{finally show} \<open>"t\<^sub>1 < t\<^sub>n"\<close>\ \texttt{.}
+\isacom{also have} \<open>"... \<le> t\<^sub>n"\<close> \isasymproof \\
+\isacom{finally show} \<open>"t\<^sub>1 < t\<^sub>n"\<close>\ \texttt{.}
\end{quote}
-The relation symbol in the \isakeyword{finally} step needs to be the most precise one
+The relation symbol in the \isacom{finally} step needs to be the most precise one
possible. In the example above, you must not write \<open>t\<^sub>1 \<le> t\<^sub>n\<close> instead of \mbox{\<open>t\<^sub>1 < t\<^sub>n\<close>}.
\begin{warn}
@@ -484,24 +484,24 @@
\end{warn}
If you want to go beyond merely using the above proof patterns and want to
-understand what \isakeyword{also} and \isakeyword{finally} mean, read on.
+understand what \isacom{also} and \isacom{finally} mean, read on.
There is an Isar theorem variable called \<open>calculation\<close>, similar to \<open>this\<close>.
-When the first \isakeyword{also} in a chain is encountered, Isabelle sets
-\<open>calculation := this\<close>. In each subsequent \isakeyword{also} step,
+When the first \isacom{also} in a chain is encountered, Isabelle sets
+\<open>calculation := this\<close>. In each subsequent \isacom{also} step,
Isabelle composes the theorems \<open>calculation\<close> and \<open>this\<close> (i.e.\ the two previous
(in)equalities) using some predefined set of rules including transitivity
of \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close> but also mixed rules like \<^prop>\<open>\<lbrakk> x \<le> y; y < z \<rbrakk> \<Longrightarrow> x < z\<close>.
The result of this composition is assigned to \<open>calculation\<close>. Consider
\begin{quote}
-\isakeyword{have} \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close> \isasymproof\\
-\isakeyword{also} \isakeyword{have} \<open>"... < t\<^sub>3"\<close> \isasymproof\\
-\isakeyword{also} \isakeyword{have} \<open>"... = t\<^sub>4"\<close> \isasymproof\\
-\isakeyword{finally show} \<open>"t\<^sub>1 < t\<^sub>4"\<close>\ \texttt{.}
+\isacom{have} \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close> \isasymproof\\
+\isacom{also} \isacom{have} \<open>"... < t\<^sub>3"\<close> \isasymproof\\
+\isacom{also} \isacom{have} \<open>"... = t\<^sub>4"\<close> \isasymproof\\
+\isacom{finally show} \<open>"t\<^sub>1 < t\<^sub>4"\<close>\ \texttt{.}
\end{quote}
-After the first \isakeyword{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close>,
-and after the second \isakeyword{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 < t\<^sub>3"\<close>.
-The command \isakeyword{finally} is short for \isakeyword{also from} \<open>calculation\<close>.
-Therefore the \isakeyword{also} hidden in \isakeyword{finally} sets \<open>calculation\<close>
+After the first \isacom{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close>,
+and after the second \isacom{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 < t\<^sub>3"\<close>.
+The command \isacom{finally} is short for \isacom{also from} \<open>calculation\<close>.
+Therefore the \isacom{also} hidden in \isacom{finally} sets \<open>calculation\<close>
to \<open>t\<^sub>1 < t\<^sub>4\<close> and the final ``\texttt{.}'' succeeds.
For more information on this style of proof see @{cite "BauerW-TPHOLs01"}.
@@ -993,7 +993,7 @@
next
case (evSS m)
have "evn(Suc(Suc m)) = evn m" by simp
- thus ?case using \<open>evn m\<close> by blast
+ thus ?case using `evn m` by blast
qed
text\<open>
--- a/src/Doc/Prog_Prove/document/prelude.tex Mon Mar 29 12:26:13 2021 +0100
+++ b/src/Doc/Prog_Prove/document/prelude.tex Tue Mar 30 09:42:25 2021 +0200
@@ -6,7 +6,9 @@
\usepackage{alltt}
\usepackage[T1]{fontenc}
-\usepackage{ccfonts}
+\usepackage[boldsans]{ccfonts}
+\DeclareFontSeriesDefault[rm]{bf}{bx}%bf default for rm: bold extended
+\DeclareFontSeriesDefault[sf]{bf}{sbc}%bf default for sf: semibold
\usepackage[euler-digits]{eulervm}
\usepackage{isabelle,isabellesym}
@@ -50,8 +52,9 @@
\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}}
% isabelle keyword, adapted from isabelle.sty
\renewcommand{\isakeyword}[1]
-{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
-\def\isacharbraceleft{\{}\def\isacharbraceright{\}}\def\bfdefault{sbc}\textbf{#1}}}
+{\emph{\sffamily\bfseries%
+\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
% add \noindent to text blocks automatically
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}