diff -r be043b89acc5 -r 77951eaeb5b0 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Tue Dec 05 18:55:45 2000 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Tue Dec 05 18:56:18 2000 +0100
@@ -92,7 +92,7 @@
 
 The following trivial proof illustrates this point. 
 \begin{isabelle}
-\isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\
+\isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\
 Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
 (Q\ \isasymand\ P)"\isanewline
 \isacommand{apply}\ (rule\ conjI)\isanewline
@@ -107,31 +107,31 @@
 (Q\ \isasymand\ P)}.  We are working backwards, so when we
 apply conjunction introduction, the rule removes the outermost occurrence
 of the \isa{\isasymand} symbol.  To apply a  rule to a subgoal, we apply
-the proof method {\isa{rule}} --- here with {\isa{conjI}}, the  conjunction
+the proof method \isa{rule} --- here with {\isa{conjI}}, the  conjunction
 introduction rule. 
 \begin{isabelle}
-%{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
+%\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\
 %\isasymand\ P\isanewline
-\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
-\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
+\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
+\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P
 \end{isabelle}
 Isabelle leaves two new subgoals: the two halves of the original conjunction. 
 The first is simply \isa{P}, which is trivial, since \isa{P} is among 
-the assumptions.  We can apply the {\isa{assumption}} 
+the assumptions.  We can apply the \isa{assumption} 
 method, which proves a subgoal by finding a matching assumption.
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ 
+\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ 
 Q\ \isasymand\ P
 \end{isabelle}
 We are left with the subgoal of proving  
 \isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}.  We apply
 \isa{rule conjI} again. 
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
-\ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
+\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline
+\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P
 \end{isabelle}
 We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved
-using the {\isa{assumption}} method. 
+using the \isa{assumption} method. 
 
 
 \section{Elimination rules}
@@ -198,12 +198,12 @@
 second assumes \isa{Q}.  Tackling the first subgoal, we need to 
 show \isa{Q\ \isasymor\ P}\@.  The second introduction rule (\isa{disjI2})
 can reduce this  to \isa{P}, which matches the assumption. So, we apply the
-{\isa{rule}}  method with \isa{disjI2} \ldots
+\isa{rule}  method with \isa{disjI2} \ldots
 \begin{isabelle}
 \ 1.\ P\ \isasymLongrightarrow\ P\isanewline
 \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P
 \end{isabelle}
-\ldots and finish off with the {\isa{assumption}} 
+\ldots and finish off with the \isa{assumption} 
 method.  We are left with the other subgoal, which 
 assumes \isa{Q}.  
 \begin{isabelle}
@@ -324,12 +324,12 @@
 \begin{isabelle}
 %P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\
 %\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline
-\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
+\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R
 \end{isabelle}
 Next, we apply conjunction elimination (\isa{erule conjE}), which splits this
 conjunction into two  parts. 
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
+\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\
 Q\isasymrbrakk\ \isasymLongrightarrow\ R
 \end{isabelle}
 Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\
@@ -340,13 +340,13 @@
 \isasymlongrightarrow\ R}, but first we must prove the extra subgoal 
 \isa{P}, which we do by assumption. 
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
-\ 2.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
+\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline
+\ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R
 \end{isabelle}
 Repeating these steps for \isa{Q\
 \isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}.
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
+\ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\
 \isasymLongrightarrow\ R
 \end{isabelle}
 
@@ -380,9 +380,9 @@
 terms. The simplest case is when the two terms  are already the same. Next
 simplest is when the variables in only one of the term
  are replaced; this is called \textbf{pattern-matching}.  The
-{\isa{rule}} method typically  matches the rule's conclusion
+\isa{rule} method typically  matches the rule's conclusion
 against the current subgoal.  In the most complex case,  variables in both
-terms are replaced; the {\isa{rule}} method can do this the goal
+terms are replaced; the \isa{rule} method can do this the goal
 itself contains schematic variables.  Other occurrences of the variables in
 the rule or proof state are updated at the same time.
 
@@ -445,10 +445,8 @@
 rule gives us more control. Consider this proof: 
 \begin{isabelle}
 \isacommand{lemma}\
-"{\isasymlbrakk}\ x\
-=\ f\ x;\ odd(f\
-x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\
-x"\isanewline
+"\isasymlbrakk \ x\ =\ f\ x;\ odd(f\ x)\ \isasymrbrakk\ \isasymLongrightarrow\
+odd\ x"\isanewline
 \isacommand{apply}\ (erule\ ssubst)\isanewline
 \isacommand{apply}\ assumption\isanewline
 \isacommand{done}\end{isabelle}
@@ -471,7 +469,7 @@
 
 Higher-order unification can be tricky, as this example indicates: 
 \begin{isabelle}
-\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\
+\isacommand{lemma}\ "\isasymlbrakk \ x\ =\
 f\ x;\ triple\ (f\ x)\
 (f\ x)\ x\ \isasymrbrakk\
 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
@@ -525,9 +523,7 @@
 use. We get a one-line proof of our example: 
 \begin{isabelle}
 \isacommand{lemma}\
-"{\isasymlbrakk}\ x\
-=\ f\ x;\ triple\ (f\
-x)\ (f\ x)\ x\
+"\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\
 \isasymrbrakk\
 \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
 \isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline
@@ -535,18 +531,16 @@
 \end{isabelle}
 
 The most general way to get rid of the {\isa{back}} command is 
-to instantiate variables in the rule.  The method {\isa{rule\_tac}} is
+to instantiate variables in the rule.  The method \isa{rule_tac} is
 similar to \isa{rule}, but it
 makes some of the rule's variables  denote specified terms.  
-Also available are {\isa{drule\_tac}}  and \isa{erule\_tac}.  Here we need
-\isa{erule\_tac} since above we used
+Also available are {\isa{drule_tac}}  and \isa{erule_tac}.  Here we need
+\isa{erule_tac} since above we used
 \isa{erule}.
 \begin{isabelle}
-\isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
-\isacommand{apply}\ (erule_tac\
-P="{\isasymlambda}u.\ triple\ u\
-u\ x"\ \isakeyword{in}\
-ssubst)\isanewline
+\isacommand{lemma}\ "\isasymlbrakk \ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline
+\isacommand{apply}\ (erule_tac\ P="{\isasymlambda}u.\ triple\ u\ u\ x"\
+\isakeyword{in}\ ssubst)\isanewline
 \isacommand{apply}\ assumption\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -557,9 +551,9 @@
 u\ x} indicate that the first two arguments have to be substituted, leaving
 the third unchanged.
 
-An alternative to {\isa{rule\_tac}} is to use \isa{rule} with the
-{\isa{of}}  directive, described in \S\ref{sec:forward} below.   An
-advantage  of {\isa{rule\_tac}} is that the instantiations may refer to 
+An alternative to \isa{rule_tac} is to use \isa{rule} with the
+\isa{of} directive, described in \S\ref{sec:forward} below.   An
+advantage  of \isa{rule_tac} is that the instantiations may refer to 
 variables bound in the current subgoal.
 
 
@@ -633,7 +627,8 @@
 
 We can now apply introduction rules.  We use the {\isa{intro}} method, which
 repeatedly  applies built-in introduction rules.  Here its effect is equivalent
-to \isa{rule impI}.\begin{isabelle}
+to \isa{rule impI}.
+\begin{isabelle}
 \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\
 R\isasymrbrakk\ \isasymLongrightarrow\ Q%
 \end{isabelle}
@@ -696,9 +691,9 @@
 \isa{Q\
 \isasymand\ R}:  
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
+\ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\
 Q\isanewline
-\ 2.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
+\ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R%
 \end{isabelle}
 The rest of the proof is trivial.
 
@@ -723,7 +718,7 @@
 Returning to the universal quantifier, we find that having a similar quantifier
 as part of the meta-logic makes the introduction rule trivial to express:
 \begin{isabelle}
-({\isasymAnd}x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
+(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI}
 \end{isabelle}
 
 
@@ -738,7 +733,7 @@
 The first step invokes the rule by applying the method \isa{rule allI}. 
 \begin{isabelle}
 %{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline
-\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymlongrightarrow\ P\ x
+\ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x
 \end{isabelle}
 Note  that the resulting proof state has a bound variable,
 namely~\bigisa{x}.  The rule has replaced the universal quantifier of
@@ -747,9 +742,9 @@
 \isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is 
 an implication, so we apply the corresponding introduction rule (\isa{impI}). 
 \begin{isabelle}
-\ 1.\ {\isasymAnd}x.\ P\ x\ \isasymLongrightarrow\ P\ x
+\ 1.\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow\ P\ x
 \end{isabelle}
-The {\isa{assumption}} method proves this last subgoal. 
+The \isa{assumption} method proves this last subgoal. 
 
 \medskip
 Now consider universal elimination. In a logic text, 
@@ -792,7 +787,7 @@
 \begin{isabelle}
 %{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x\ \isasymLongrightarrow\ P\
 %\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)\isanewline
-\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
+\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
 \end{isabelle}
 As before, it replaces the HOL 
 quantifier by a meta-level quantifier, producing a subgoal that 
@@ -809,8 +804,8 @@
 method.  This rule is called \isa{spec} because it specializes a universal formula
 to a particular term.
 \begin{isabelle}
-\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
-x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x
+\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\
+x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x
 \end{isabelle}
 Observe how the context has changed.  The quantified formula is gone,
 replaced by a new assumption derived from its body.  Informally, we have
@@ -822,7 +817,7 @@
 an implication, so we can  use \emph{modus ponens} on it. As before, it requires
 proving the  antecedent (in this case \isa{P}) and leaves us with the consequent. 
 \begin{isabelle}
-\ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ Q\ (?x2\ x){\isasymrbrakk}\
+\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\
 \isasymLongrightarrow\ Q\ x
 \end{isabelle}
 The consequent is \isa{Q} applied to that placeholder.  It may be replaced by any
@@ -889,7 +884,7 @@
 %
 It looks like this in Isabelle: 
 \begin{isabelle}
-\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ {\isasymAnd}x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
+\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE}
 \end{isabelle}
 %
 Given an existentially quantified theorem and some
@@ -943,13 +938,13 @@
 \begin{isabelle}
 %({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\
 %\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline
-\ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
+\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
 \end{isabelle}
 %
 When we remove the other quantifier, we get a different bound 
 variable in the subgoal.  (The name \isa{xa} is generated automatically.)
 \begin{isabelle}
-\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
+\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
 \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x
 \end{isabelle}
 The proviso of the existential elimination rule has forced the variables to
@@ -961,15 +956,15 @@
 and the other to become~\bigisa{xa}, but Isabelle requires all instances of a
 placeholder to be identical. 
 \begin{isabelle}
-\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
+\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
 \isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline
-\ 2.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
+\ 2.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa)
 \end{isabelle}
 We can prove either subgoal 
 using the \isa{assumption} method.  If we prove the first one, the placeholder
 changes  into~\bigisa{x}. 
 \begin{isabelle}
-\ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\
+\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\
 \isasymLongrightarrow\ Q\ x
 \end{isabelle}
 We are left with a subgoal that cannot be proved, 
@@ -1007,13 +1002,13 @@
 Next, we remove the universal quantifier 
 from the conclusion, putting the bound variable~\isa{y} into the subgoal. 
 \begin{isabelle}
-\ 1.\ {\isasymAnd}y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y
+\ 1.\ \isasymAnd y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y
 \end{isabelle}
 Finally, we try to apply our reflexivity assumption.  We obtain a 
 new assumption whose identical placeholders may be replaced by 
 any term involving~\bigisa{y}. 
 \begin{isabelle}
-\ 1.\ {\isasymAnd}y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
+\ 1.\ \isasymAnd y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y
 \end{isabelle}
 This subgoal can only be proved by putting \bigisa{y} for all the placeholders,
 making the assumption and conclusion become \isa{R\ y\ y}. 
@@ -1036,7 +1031,7 @@
 discussed, concerning negation and disjunction.  Isabelle's
 \textbf{classical reasoner} is a family of tools that perform such
 proofs automatically.  The most important of these is the 
-{\isa{blast}} method. 
+\isa{blast} method. 
 
 In this section, we shall first see how to use the classical 
 reasoner in its default mode and then how to insert additional 
@@ -1048,7 +1043,7 @@
 \footnote{Pelletier~\cite{pelletier86} describes it and many other
 problems for automatic theorem provers.}
 The nested biconditionals cause an exponential explosion: the formal
-proof is  enormous.  However, the {\isa{blast}} method proves it in
+proof is  enormous.  However, the \isa{blast} method proves it in
 a fraction  of a second. 
 \begin{isabelle}
 \isacommand{lemma}\
@@ -1072,7 +1067,7 @@
 \isacommand{done}
 \end{isabelle}
 The next example is a logic problem composed by Lewis Carroll. 
-The {\isa{blast}} method finds it trivial. Moreover, it turns out 
+The \isa{blast} method finds it trivial. Moreover, it turns out 
 that not all of the assumptions are necessary. We can easily 
 experiment with variations of this formula and see which ones 
 can be proved. 
@@ -1108,7 +1103,7 @@
 \isacommand{apply}\ blast\isanewline
 \isacommand{done}
 \end{isabelle}
-The {\isa{blast}} method is also effective for set theory, which is
+The \isa{blast} method is also effective for set theory, which is
 described in the next chapter.  This formula below may look horrible, but
 the \isa{blast} method proves it easily. 
 \begin{isabelle}
@@ -1133,7 +1128,7 @@
 An important special case avoids all these complications.  A logical 
 equivalence, which in higher-order logic is an equality between 
 formulas, can be given to the classical 
-reasoner and simplifier by using the attribute {\isa{iff}}.  You 
+reasoner and simplifier by using the attribute \isa{iff}.  You 
 should do so if the right hand side of the equivalence is  
 simpler than the left-hand side.  
 
@@ -1141,7 +1136,7 @@
 The result of appending two lists is empty if and only if both 
 of the lists are themselves empty. Obviously, applying this equivalence 
 will result in a simpler goal. When stating this lemma, we include 
-the {\isa{iff}} attribute. Once we have proved the lemma, Isabelle 
+the \isa{iff} attribute. Once we have proved the lemma, Isabelle 
 will make it known to the classical reasoner (and to the simplifier). 
 \begin{isabelle}
 \isacommand{lemma}\
@@ -1159,17 +1154,17 @@
 \end{isabelle}
 %
 This fact about multiplication is also appropriate for 
-the {\isa{iff}} attribute:\REMARK{the ?s are ugly here but we need
+the \isa{iff} attribute:\REMARK{the ?s are ugly here but we need
 them again when talking about \isa{of}; we need a consistent style}
 \begin{isabelle}
-(\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
+(\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0)
 \end{isabelle}
 A product is zero if and only if one of the factors is zero.  The
 reasoning  involves a logical \textsc{or}.  Proving new rules for
 disjunctive reasoning  is hard, but translating to an actual disjunction
 works:  the classical reasoner handles disjunction properly.
 
-In more detail, this is how the {\isa{iff}} attribute works.  It converts
+In more detail, this is how the \isa{iff} attribute works.  It converts
 the equivalence $P=Q$ to a pair of rules: the introduction
 rule $Q\Imp P$ and the destruction rule $P\Imp Q$.  It gives both to the
 classical reasoner as safe rules, ensuring that all occurrences of $P$ in
@@ -1186,23 +1181,23 @@
 
 A brief development will illustrate advanced use of  
 \isa{blast}.  In \S\ref{sec:recdef-simplification}, we declared the
-recursive function {\isa{gcd}}:
+recursive function \isa{gcd}:
 \begin{isabelle}
-\isacommand{consts}\ gcd\ ::\ "nat{\isacharasterisk}nat\ \isasymRightarrow\ nat"\
+\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\
 \
 \
 \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
 \isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\
-::nat{\isacharasterisk}nat\ \isasymRightarrow\ nat)"\isanewline
+::nat*nat\ \isasymRightarrow\ nat)"\isanewline
 \ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
 \end{isabelle}
 Let us prove that it computes the greatest common
 divisor of its two arguments.  
 %
 %The declaration yields a recursion
-%equation  for {\isa{gcd}}.  Simplifying with this equation can 
+%equation  for \isa{gcd}.  Simplifying with this equation can 
 %cause looping, expanding to ever-larger expressions of if-then-else 
-%and {\isa{gcd}} calls.  To prevent this, we prove separate simplification rules
+%and \isa{gcd} calls.  To prevent this, we prove separate simplification rules
 %for $n=0$\ldots
 %\begin{isabelle}
 %\isacommand{lemma}\ gcd_0\ [simp]:\ "gcd(m,0)\ =\ m"\isanewline
@@ -1219,18 +1214,18 @@
 %does not loop because it is conditional.  It can be applied only
 %when the second argument is known to be non-zero.
 %Armed with our two new simplification rules, we now delete the 
-%original {\isa{gcd}} recursion equation. 
+%original \isa{gcd} recursion equation. 
 %\begin{isabelle}
 %\isacommand{declare}\ gcd.simps\ [simp\ del]
 %\end{isabelle}
 %
-%Now we can prove  some interesting facts about the {\isa{gcd}} function,
+%Now we can prove  some interesting facts about the \isa{gcd} function,
 %for exampe, that it computes a common divisor of its arguments.  
 %
 The theorem is expressed in terms of the familiar
 \textbf{divides} relation from number theory: 
 \begin{isabelle}
-?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ \isacharasterisk\ k
+?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k
 \rulename{dvd_def}
 \end{isabelle}
 %
@@ -1251,12 +1246,12 @@
 half of the conjunction establishes the other. The first three proof steps 
 are applying induction, performing a case analysis on \isa{n}, 
 and simplifying.  Let us pass over these quickly and consider
-the use of {\isa{blast}}.  We have reached the following 
+the use of \isa{blast}.  We have reached the following 
 subgoal: 
 \begin{isabelle}
 %gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline
-\ 1.\ {\isasymAnd}m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline
- \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n){\isasymrbrakk}\isanewline
+\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline
+ \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m
 \end{isabelle}
 %
@@ -1292,7 +1287,7 @@
 tells Isabelle to transform a theorem in some way and to
 give a name to the resulting theorem.  Attributes can be given,
 here \isa{iff}, which supplies the new theorems to the classical reasoner
-and the simplifier.  The directive {\isa{THEN}}, which will be explained
+and the simplifier.  The directive \isa{THEN}, which will be explained
 below, supplies the lemma 
 \isa{gcd_dvd_both} to the
 destruction rule \isa{conjunct1} in order to extract the first part.
@@ -1313,7 +1308,7 @@
 \end{isabelle}
 Later, we shall explore this type of forward reasoning in detail. 
 
-To complete the verification of the {\isa{gcd}} function, we must 
+To complete the verification of the \isa{gcd} function, we must 
 prove that it returns the greatest of all the common divisors 
 of its arguments.  The proof is by induction and simplification.
 \begin{isabelle}
@@ -1347,12 +1342,12 @@
 \isacommand{apply}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)\isanewline
 \isacommand{done}
 \end{isabelle}
-This theorem concisely expresses the correctness of the {\isa{gcd}} 
+This theorem concisely expresses the correctness of the \isa{gcd} 
 function. 
-We state it with the {\isa{iff}} attribute so that 
-Isabelle can use it to remove some occurrences of {\isa{gcd}}. 
+We state it with the \isa{iff} attribute so that 
+Isabelle can use it to remove some occurrences of \isa{gcd}. 
 The theorem has a one-line 
-proof using {\isa{blast}} supplied with four introduction 
+proof using \isa{blast} supplied with four introduction 
 rules: note the {\isa{intro}} attribute. The exclamation mark 
 ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are 
 applied aggressively.  Rules given without the exclamation mark 
@@ -1374,7 +1369,7 @@
 
 \section{Other classical reasoning methods}
  
-The {\isa{blast}} method is our main workhorse for proving theorems 
+The \isa{blast} method is our main workhorse for proving theorems 
 automatically. Other components of the classical reasoner interact 
 with the simplifier. Still others perform classical reasoning 
 to a limited extent, giving the user fine control over the proof. 
@@ -1393,10 +1388,10 @@
 \isasymand\ Q\ x)"\isanewline
 \isacommand{apply}\ clarify
 \end{isabelle}
-The {\isa{blast}} method would simply fail, but {\isa{clarify}} presents 
+The \isa{blast} method would simply fail, but {\isa{clarify}} presents 
 a subgoal that helps us see why we cannot continue the proof. 
 \begin{isabelle}
-\ 1.\ {\isasymAnd}x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
+\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\
 xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x
 \end{isabelle}
 The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x}
@@ -1423,8 +1418,8 @@
 its goal, so it can take much longer to terminate.
 
 Older components of the classical reasoner have largely been 
-superseded by {\isa{blast}}, but they still have niche applications. 
-Most important among these are {\isa{fast}} and {\isa{best}}. While {\isa{blast}} 
+superseded by \isa{blast}, but they still have niche applications. 
+Most important among these are \isa{fast} and \isa{best}. While \isa{blast} 
 searches for proofs using a built-in first-order reasoner, these 
 earlier methods search for proofs using standard Isabelle inference. 
 That makes them slower but enables them to work correctly in the 
@@ -1439,7 +1434,7 @@
 The repeated occurrence of the variable \isa{?P} makes this rule tricky 
 to apply. Consider this contrived example: 
 \begin{isabelle}
-\isacommand{lemma}\ "{\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\isanewline
+\isacommand{lemma}\ "\isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\isanewline
 \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\
 \isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline
 \isacommand{apply}\ (rule\ someI)
@@ -1448,21 +1443,21 @@
 We can apply rule \isa{someI} explicitly.  It yields the 
 following subgoal: 
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
+\ 1.\ \isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\
 \isasymand\ Q\ ?x%
 \end{isabelle}
 The proof from this point is trivial.  The question now arises, could we have
-proved the theorem with a single command? Not using {\isa{blast}} method: it
+proved the theorem with a single command? Not using \isa{blast} method: it
 cannot perform  the higher-order unification that is necessary here.  The
-{\isa{fast}}  method succeeds: 
+\isa{fast} method succeeds: 
 \begin{isabelle}
 \isacommand{apply}\ (fast\ intro!:\ someI)
 \end{isabelle}
 
-The {\isa{best}} method is similar to {\isa{fast}} but it uses a 
+The \isa{best} method is similar to \isa{fast} but it uses a 
 best-first search instead of depth-first search. Accordingly, 
 it is slower but is less susceptible to divergence. Transitivity 
-rules usually cause {\isa{fast}} to loop where often {\isa{best}} 
+rules usually cause \isa{fast} to loop where often \isa{best} 
 can manage.
 
 Here is a summary of the classical reasoning methods:
@@ -1512,7 +1507,7 @@
 Now let us reproduce our examples in Isabelle.  Here is the distributive
 law:
 \begin{isabelle}%
-?k\ \isacharasterisk\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ \isacharasterisk\ ?m,\ ?k\ \isacharasterisk\ ?n)
+?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n)
 \rulename{gcd_mult_distrib2}
 \end{isabelle}%
 The first step is to replace \isa{?m} by~1 in this law.  We refer to the
@@ -1529,7 +1524,7 @@
 \isa{thm gcd_mult_0}
 displays the resulting theorem:
 \begin{isabelle}
-\ \ \ \ \ k\ \isacharasterisk\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ \isacharasterisk\ 1,\ k\ \isacharasterisk\ ?n)
+\ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n)
 \end{isabelle}
 Something is odd: {\isa{k}} is an ordinary variable, while {\isa{?n}} 
 is schematic.  We did not specify an instantiation 
@@ -1549,7 +1544,7 @@
 %
 Again, we display the resulting theorem:
 \begin{isabelle}
-\ \ \ \ \ k\ =\ gcd\ (k,\ k\ \isacharasterisk\ ?n)
+\ \ \ \ \ k\ =\ gcd\ (k,\ k\ *\ ?n)
 \end{isabelle}
 %
 To re-orient the equation requires the symmetry rule:
@@ -1567,12 +1562,11 @@
 %
 Here is the result:
 \begin{isabelle}
-\ \ \ \ \ gcd\ (k,\ k\ \isacharasterisk\
-?n)\ =\ k%
+\ \ \ \ \ gcd\ (k,\ k\ *\ ?n)\ =\ k%
 \end{isabelle}
 \isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the
 resulting conclusion.\REMARK{figure necessary?}  The effect is to exchange the
-two operands of the equality. Typically {\isa{THEN}} is used with destruction
+two operands of the equality. Typically \isa{THEN} is used with destruction
 rules.  Above we have used
 \isa{THEN~conjunct1} to extract the first part of the theorem
 \isa{gcd_dvd_both}.  Also useful is \isa{THEN~spec}, which removes the quantifier
@@ -1581,13 +1575,10 @@
 Similar to \isa{mp} are the following two rules, which extract 
 the two directions of reasoning about a boolean equivalence:
 \begin{isabelle}
-\isasymlbrakk?Q\ =\
-?P;\ ?Q\isasymrbrakk\
-\isasymLongrightarrow\ ?P%
+\isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
 \rulename{iffD1}%
 \isanewline
-\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\
-\isasymLongrightarrow\ ?P%
+\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P%
 \rulename{iffD2}
 \end{isabelle}
 %
@@ -1609,9 +1600,7 @@
 \begin{isabelle}
 \isacommand{lemma}\ gcd_mult\
 [simp]:\
-"gcd(k,\
-k{\isacharasterisk}n)\ =\
-k"\isanewline
+"gcd(k,\ k*n)\ =\ k"\isanewline
 \isacommand{apply}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -1633,7 +1622,7 @@
 instance of a rule by specifying facts for its premises.  Let us try
 it with this rule:
 \begin{isabelle}
-{\isasymlbrakk}gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n){\isasymrbrakk}\
+\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n)\isasymrbrakk\
 \isasymLongrightarrow\ ?k\ dvd\ ?m
 \rulename{relprime_dvd_mult}
 \end{isabelle}
@@ -1648,24 +1637,23 @@
 simplification.  Expression evaluation  is not guaranteed to terminate, and
 certainly is not  efficient; Isabelle performs arithmetic operations by 
 rewriting symbolic bit strings.  Here, however, the simplification takes
-less than one second.  We can specify this new lemma to {\isa{OF}},
+less than one second.  We can specify this new lemma to \isa{OF},
 generating an instance of \isa{relprime_dvd_mult}.  The expression
 \begin{isabelle}
 \ \ \ \ \ relprime_dvd_mult [OF relprime_20_81]
 \end{isabelle}
 yields the theorem
 \begin{isabelle}
-\ \ \ \ \ \isacharhash20\ dvd\ (?m\ \isacharasterisk\ \isacharhash81)\ \isasymLongrightarrow\ \isacharhash20\ dvd\ ?m%
+\ \ \ \ \ \#20\ dvd\ (?m\ *\ \#81)\ \isasymLongrightarrow\ \#20\ dvd\ ?m%
 \end{isabelle}
 %
-{\isa{OF}} takes any number of operands.  Consider 
+\isa{OF} takes any number of operands.  Consider 
 the following facts about the divides relation: 
 \begin{isabelle}
 \isasymlbrakk?k\ dvd\ ?m;\
 ?k\ dvd\ ?n\isasymrbrakk\
 \isasymLongrightarrow\ ?k\ dvd\
-(?m\ \isacharplus\
-?n)
+(?m\ +\ ?n)
 \rulename{dvd_add}\isanewline
 ?m\ dvd\ ?m%
 \rulename{dvd_refl}
@@ -1676,7 +1664,7 @@
 \end{isabelle}
 Here is the theorem that we have expressed: 
 \begin{isabelle}
-\ \ \ \ \ ?k\ dvd\ (?k\ \isacharplus\ ?k)
+\ \ \ \ \ ?k\ dvd\ (?k\ +\ ?k)
 \end{isabelle}
 As with \isa{of}, we can use the \isa{_} symbol to leave some positions
 unspecified:
@@ -1685,10 +1673,10 @@
 \end{isabelle}
 The result is 
 \begin{isabelle}
-\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ \isacharplus\ ?k)
+\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ +\ ?k)
 \end{isabelle}
 
-You may have noticed that {\isa{THEN}} and {\isa{OF}} are based on 
+You may have noticed that \isa{THEN} and \isa{OF} are based on 
 the same idea, namely to combine two rules.  They differ in the
 order of the combination and thus in their effect.  We use \isa{THEN}
 typically with a destruction rule to extract a subformula of the current
@@ -1698,9 +1686,9 @@
 
 Here is a summary of the primitives for forward reasoning:
 \begin{itemize}
-\item {\isa{of}} instantiates the variables of a rule to a list of terms
-\item {\isa{OF}} applies a rule to a list of theorems
-\item {\isa{THEN}} gives a theorem to a named rule and returns the
+\item \isa{of} instantiates the variables of a rule to a list of terms
+\item \isa{OF} applies a rule to a list of theorems
+\item \isa{THEN} gives a theorem to a named rule and returns the
 conclusion 
 \end{itemize}
 
@@ -1711,7 +1699,7 @@
 proof.  Also in that spirit is the \isa{insert} method, which inserts a
 given theorem as a new assumption of the current subgoal.  This already
 is a forward step; moreover, we may (as always when using a theorem) apply
-{\isa{of}}, {\isa{THEN}} and other directives.  The new assumption can then
+\isa{of}, \isa{THEN} and other directives.  The new assumption can then
 be used to help prove the subgoal.
 
 For example, consider this theorem about the divides relation. 
@@ -1720,9 +1708,9 @@
 \begin{isabelle}
 \isacommand{lemma}\
 relprime_dvd_mult:\isanewline
-\ \ \ \ \ \ \ "{\isasymlbrakk}\ gcd(k,n){=}1;\
+\ \ \ \ \ \ \ "\isasymlbrakk \ gcd(k,n){=}1;\
 k\ dvd\ (m*n)\
-{\isasymrbrakk}\
+\isasymrbrakk\
 \isasymLongrightarrow\ k\ dvd\
 m"\isanewline
 \isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\
@@ -1731,31 +1719,25 @@
 In the resulting subgoal, note how the equation has been 
 inserted: 
 \begin{isabelle}
-{\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\
-dvd\ (m\ \isacharasterisk\
-n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\
+\isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\
+dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
 m\isanewline
-\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline
-\ \ \ \ \ m\ \isacharasterisk\ gcd\
+\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
+\ \ \ \ \ m\ *\ gcd\
 (k,\ n)\
-=\ gcd\ (m\ \isacharasterisk\
-k,\ m\ \isacharasterisk\
-n){\isasymrbrakk}\isanewline
+=\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
 \end{isabelle}
 The next proof step, \isa{\isacommand{apply}(simp)}, 
 utilizes the assumption \isa{gcd(k,n)\ =\
 1}. Here is the result: 
 \begin{isabelle}
-{\isasymlbrakk}gcd\ (k,\
+\isasymlbrakk gcd\ (k,\
 n)\ =\ 1;\ k\
-dvd\ (m\ \isacharasterisk\
-n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\
+dvd\ (m\ *\ n)\isasymrbrakk\ \isasymLongrightarrow\ k\ dvd\
 m\isanewline
-\ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline
-\ \ \ \ \ m\ =\ gcd\ (m\
-\isacharasterisk\ k,\ m\ \isacharasterisk\
-n){\isasymrbrakk}\isanewline
+\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;}\isanewline
+\ \ \ \ \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
 \end{isabelle}
 Simplification has yielded an equation for \isa{m} that will be used to
@@ -1765,17 +1747,16 @@
 Here is another proof using \isa{insert}.  \REMARK{Effect with unknowns?}
 Division  and remainder obey a well-known law: 
 \begin{isabelle}
-(?m\ div\ ?n)\ \isacharasterisk\
-?n\ \isacharplus\ ?m\ mod\ ?n\
-=\ ?m
+(?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
 \rulename{mod_div_equality}
 \end{isabelle}
 
 We refer to this law explicitly in the following proof: 
 \begin{isabelle}
 \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
-\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m{\isacharasterisk}n)\ div\ n\ =\ (m::nat)"\isanewline
-\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m{\isacharasterisk}n"\ n])\isanewline
+\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\
+(m::nat)"\isanewline
+\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline
 \isacommand{apply}\ (simp)\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -1785,20 +1766,19 @@
 subgoal, with its new assumption: 
 \begin{isabelle}
 %0\ \isacharless\ n\ \isasymLongrightarrow\ (m\
-%\isacharasterisk\ n)\ div\ n\ =\ m\isanewline
+%*\ n)\ div\ n\ =\ m\isanewline
 \ 1.\ \isasymlbrakk0\ \isacharless\
-n;\ \ (m\ \isacharasterisk\ n)\ div\ n\
-\isacharasterisk\ n\ \isacharplus\ (m\ \isacharasterisk\ n)\ mod\ n\
-=\ m\ \isacharasterisk\ n\isasymrbrakk\isanewline
-\ \ \ \ \isasymLongrightarrow\ (m\ \isacharasterisk\ n)\ div\ n\
+n;\ \ (m\ *\ n)\ div\ n\ *\ n\ +\ (m\ *\ n)\ mod\ n\
+=\ m\ *\ n\isasymrbrakk\isanewline
+\ \ \ \ \isasymLongrightarrow\ (m\ *\ n)\ div\ n\
 =\ m
 \end{isabelle}
-Simplification reduces \isa{(m\ \isacharasterisk\ n)\ mod\ n} to zero.
+Simplification reduces \isa{(m\ *\ n)\ mod\ n} to zero.
 Then it cancels the factor~\isa{n} on both
 sides of the equation, proving the theorem. 
 
 \medskip
-A similar method is {\isa{subgoal\_tac}}. Instead of inserting 
+A similar method is {\isa{subgoal_tac}}. Instead of inserting 
 a theorem as an assumption, it inserts an arbitrary formula. 
 This formula must be proved later as a separate subgoal. The 
 idea is to claim that the formula holds on the basis of the current 
@@ -1830,25 +1810,25 @@
 step is to claim that \isa{z} is either 34 or 36. The resulting proof 
 state gives us two subgoals: 
 \begin{isabelle}
-%{\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\
+%\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\
 %Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline
-\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
+\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
 \ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline
-\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
+\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
 \end{isabelle}
 
 The first subgoal is trivial, but for the second Isabelle needs help to eliminate
 the case
-\isa{z}=35.  The second invocation  of {\isa{subgoal\_tac}} leaves two
+\isa{z}=35.  The second invocation  of {\isa{subgoal_tac}} leaves two
 subgoals: 
 \begin{isabelle}
-\ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\
+\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\
 \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline
 \ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline
-\ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
+\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline
 \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
 \end{isabelle}