# HG changeset patch
# User nipkow
# Date 1617090145 -7200
# Node ID 2cdbb6a2f2a7ad98aacded28863e705408e499f5
# Parent  c526eb2c7ca0cb3488384c4c2cc7dcdba2ac1def
updated to latest latex due to new mechanism for dealing with bold ccfonts

diff -r c526eb2c7ca0 -r 2cdbb6a2f2a7 src/Doc/Prog_Prove/Basics.thy
--- 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
diff -r c526eb2c7ca0 -r 2cdbb6a2f2a7 src/Doc/Prog_Prove/Bool_nat_list.thy
--- 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))"
 
diff -r c526eb2c7ca0 -r 2cdbb6a2f2a7 src/Doc/Prog_Prove/Isar.thy
--- 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>
diff -r c526eb2c7ca0 -r 2cdbb6a2f2a7 src/Doc/Prog_Prove/document/prelude.tex
--- 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}}