diff -r b247e62520ec -r 8a5aa26c125f doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Mon Oct 23 17:37:20 2000 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Mon Oct 23 17:37:49 2000 +0200
@@ -94,7 +94,7 @@
 \begin{isabelle}
 \isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\
 Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\
-(Q\ \isasymand\ P){"}\isanewline
+(Q\ \isasymand\ P)"\isanewline
 \isacommand{apply}\ (rule\ conjI)\isanewline
 \ \isacommand{apply}\ assumption\isanewline
 \isacommand{apply}\ (rule\ conjI)\isanewline
@@ -172,7 +172,7 @@
 a case split.  (We have this before, in proofs by induction.)  The following  proof
 illustrates the use of disjunction elimination.  
 \begin{isabelle}
-\isacommand{lemma}\ disj_swap:\ {"}P\ \isasymor\ Q\ 
+\isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ 
 \isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline
 \isacommand{apply}\ (erule\ disjE)\isanewline
 \ \isacommand{apply}\ (rule\ disjI2)\isanewline
@@ -223,7 +223,7 @@
 
 Now let us examine the analogous proof for conjunction. 
 \begin{isabelle}
-\isacommand{lemma}\ conj_swap:\ {"}P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline
+\isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline
 \isacommand{apply}\ (rule\ conjI)\isanewline
 \ \isacommand{apply}\ (drule\ conjunct2)\isanewline
 \ \isacommand{apply}\ assumption\isanewline
@@ -234,7 +234,7 @@
 \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
 of a conjunction.  Rules of this sort (where the conclusion is a subformula of a
 premise) are called \textbf{destruction} rules, by analogy with the destructor
-functions of functional pr§gramming.%
+functions of functional programming.%
 \footnote{This Isabelle terminology has no counterpart in standard logic texts, 
 although the distinction between the two forms of elimination rule is well known. 
 Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules are very
@@ -307,7 +307,7 @@
 of a nested implication by a conjunction. 
 \begin{isabelle}
 \isacommand{lemma}\ imp_uncurry:\
-{"}P\ \isasymlongrightarrow\ (Q\
+"P\ \isasymlongrightarrow\ (Q\
 \isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\
 \isasymand\ Q\ \isasymlongrightarrow\
 R"\isanewline
@@ -371,10 +371,6 @@
 \S\ref{sec:proving-euclid}.
 
 
-
-\remark{negation: notI, notE, ccontr, swap, contrapos?}
-
-
 \section{Unification and substitution}\label{sec:unification}
 
 As we have seen, Isabelle rules involve variables that begin  with a
@@ -548,7 +544,7 @@
 \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\
+P="{\isasymlambda}u.\ triple\ u\
 u\ x"\ \isakeyword{in}\
 ssubst)\isanewline
 \isacommand{apply}\ assumption\isanewline
@@ -695,7 +691,7 @@
 \ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI)
 \end{isabelle}
 is robust: the \isa{conjI} forces the \isa{erule} to select a
-conjunction.  The two subgoals are the ones we would expect from appling
+conjunction.  The two subgoals are the ones we would expect from applying
 conjunction introduction to
 \isa{Q\
 \isasymand\ R}:  
@@ -782,7 +778,7 @@
 \begin{isabelle}
 \isacommand{lemma}\ "({\isasymforall}x.\ P\
 \isasymlongrightarrow\ Q\ x)\ \isasymLongrightarrow\ P\
-\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x){"}\isanewline
+\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)"\isanewline
 \isacommand{apply}\ (rule\ impI)\isanewline
 \isacommand{apply}\ (rule\ allI)\isanewline
 \isacommand{apply}\ (drule\ spec)\isanewline
@@ -911,7 +907,7 @@
 This rule is seldom used, for it can cause exponential blow-up.  The
 main use of $\epsilon x. P(x)$ is in definitions when $P(x)$ characterizes $x$
 uniquely.  For instance, we can define the cardinality of a finite set~$A$ to be that
-$n$ such that $A$ is in one-to-one correspondance with $\{1,\ldots,n\}$.  We can then
+$n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$.  We can then
 prove that the cardinality of the empty set is zero (since $n=0$ satisfies the
 description) and proceed to prove other facts.\remark{SOME theorems
 and example}
@@ -1058,20 +1054,20 @@
 \isacommand{lemma}\
 "(({\isasymexists}x.\
 {\isasymforall}y.\
-p(x){=}p(y){)}\
+p(x){=}p(y))\
 =\
 (({\isasymexists}x.\
-q(x){)}=({\isasymforall}y.\
-p(y){)}){)}\
+q(x))=({\isasymforall}y.\
+p(y))))\
 \ \ =\ \ \ \ \isanewline
 \ \ \ \ \ \ \ \
 (({\isasymexists}x.\
 {\isasymforall}y.\
-q(x){=}q(y){)}\
+q(x){=}q(y))\
 =\
 (({\isasymexists}x.\
-p(x){)}=({\isasymforall}y.\
-q(y){)}){)}"\isanewline
+p(x))=({\isasymforall}y.\
+q(y))))"\isanewline
 \isacommand{apply}\ blast\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -1085,30 +1081,30 @@
 "({\isasymforall}x.\
 honest(x)\ \isasymand\
 industrious(x)\ \isasymlongrightarrow\
-healthy(x){)}\
+healthy(x))\
 \isasymand\ \ \isanewline
 \ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\
 grocer(x)\ \isasymand\
-healthy(x){)}\
+healthy(x))\
 \isasymand\ \isanewline
 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
 industrious(x)\ \isasymand\
 grocer(x)\ \isasymlongrightarrow\
-honest(x){)}\
+honest(x))\
 \isasymand\ \isanewline
 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
 cyclist(x)\ \isasymlongrightarrow\
-industrious(x){)}\
+industrious(x))\
 \isasymand\ \isanewline
 \ \ \ \ \ \ \ \ ({\isasymforall}x.\
 {\isasymnot}healthy(x)\ \isasymand\
 cyclist(x)\ \isasymlongrightarrow\
-{\isasymnot}honest(x){)}\
+{\isasymnot}honest(x))\
 \ \isanewline
 \ \ \ \ \ \ \ \ \isasymlongrightarrow\
 ({\isasymforall}x.\
 grocer(x)\ \isasymlongrightarrow\
-{\isasymnot}cyclist(x){)}"\isanewline
+{\isasymnot}cyclist(x))"\isanewline
 \isacommand{apply}\ blast\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -1116,8 +1112,8 @@
 described in the next chapter.  This formula below may look horrible, but
 the \isa{blast} method proves it easily. 
 \begin{isabelle}
-\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i){)}\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j){)}\ =\isanewline
-\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j){)}"\isanewline
+\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline
+\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline
 \isacommand{apply}\ blast\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -1149,12 +1145,12 @@
 will make it known to the classical reasoner (and to the simplifier). 
 \begin{isabelle}
 \isacommand{lemma}\
-[iff]{:}\
+[iff]:\
 "(xs{\isacharat}ys\ =\
 \isacharbrackleft{]})\ =\
 (xs=[]\
 \isacharampersand\
-ys=[]{)}"\isanewline
+ys=[])"\isanewline
 \isacommand{apply}\ (induct_tac\
 xs)\isanewline
 \isacommand{apply}\ (simp_all)
@@ -1192,9 +1188,13 @@
 \isa{blast}.  In \S\ref{sec:recdef-simplification}, we declared the
 recursive function {\isa{gcd}}:
 \begin{isabelle}
-\isacommand{consts}\ gcd\ :{:}\ {"}nat{\isacharasterisk}nat={\isachargreater}nat"\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline
-\isacommand{recdef}\ gcd\ {"}measure\ ((\isasymlambda(m{,}n){.}n)\ :{:}nat{\isacharasterisk}nat={\isachargreater}nat){"}\isanewline
-\ \ \ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n){)}"%
+\isacommand{consts}\ gcd\ ::\ "nat{\isacharasterisk}nat\ \isasymRightarrow\ nat"\
+\
+\
+\ \ \ \ \ \ \ \ \ \ \ \ \isanewline
+\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\
+::nat{\isacharasterisk}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.  
@@ -1205,13 +1205,13 @@
 %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
+%\isacommand{lemma}\ gcd_0\ [simp]:\ "gcd(m,0)\ =\ m"\isanewline
 %\isacommand{apply}\ (simp)\isanewline
 %\isacommand{done}
 %\end{isabelle}
 %\ldots{} and for $n>0$:
 %\begin{isabelle}
-%\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m{,}n)\ =\ gcd\ (n,\ m\ mod\ n){"}\isanewline
+%\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m,n)\ =\ gcd\ (n,\ m\ mod\ n)"\isanewline
 %\isacommand{apply}\ (simp)\isanewline
 %\isacommand{done}
 %\end{isabelle}
@@ -1221,7 +1221,7 @@
 %Armed with our two new simplification rules, we now delete the 
 %original {\isa{gcd}} recursion equation. 
 %\begin{isabelle}
-%\isacommand{declare}\ gcd{.}simps\ [simp\ del]
+%\isacommand{declare}\ gcd.simps\ [simp\ del]
 %\end{isabelle}
 %
 %Now we can prove  some interesting facts about the {\isa{gcd}} function,
@@ -1239,9 +1239,9 @@
 rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the
 definition of \isa{gcd} can cause looping.
 \begin{isabelle}
-\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m{,}n)\ dvd\ m)\ \isasymand\ (gcd(m{,}n)\ dvd\ n){"}\isanewline
-\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd{.}induct)\isanewline
-\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline
+\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ n)"\isanewline
+\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline
+\isacommand{apply}\ (case_tac\ "n=0")\isanewline
 \isacommand{apply}\ (simp_all)\isanewline
 \isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline
 \isacommand{done}%
@@ -1273,7 +1273,7 @@
 \isa{?k\ dvd\ ?m}) to the two premises, which 
 also involve the divides relation. This process does not look promising
 and could easily loop.  More sensible is  to apply the rule in the forward
-direction; each step would eliminate  the \isa{mod} symboi from an
+direction; each step would eliminate  the \isa{mod} symbol from an
 assumption, so the process must terminate.  
 
 So the final proof step applies the \isa{blast} method.
@@ -1318,14 +1318,14 @@
 of its arguments.  The proof is by induction and simplification.
 \begin{isabelle}
 \isacommand{lemma}\ gcd_greatest\
-[rule_format]{:}\isanewline
+[rule_format]:\isanewline
 \ \ \ \ \ \ \ "(k\ dvd\
 m)\ \isasymlongrightarrow\ (k\ dvd\
 n)\ \isasymlongrightarrow\ k\ dvd\
-gcd(m{,}n)"\isanewline
+gcd(m,n)"\isanewline
 \isacommand{apply}\ (induct_tac\ m\ n\
-rule:\ gcd{.}induct)\isanewline
-\isacommand{apply}\ (case_tac\ "n=0"{)}\isanewline
+rule:\ gcd.induct)\isanewline
+\isacommand{apply}\ (case_tac\ "n=0")\isanewline
 \isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -1342,9 +1342,9 @@
 equivalence.  This step gives us a chance to see another application
 of \isa{blast}, and it is worth doing for sound logical reasons.
 \begin{isabelle}
-\isacommand{theorem}\ gcd_greatest_iff\ [iff]{:}\isanewline
-\ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m{,}n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline
-\isacommand{apply}\ (blast\ intro!{:}\ gcd_greatest\ intro:\ dvd_trans)\isanewline
+\isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline
+\ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m,n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline
+\isacommand{apply}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)\isanewline
 \isacommand{done}
 \end{isabelle}
 This theorem concisely expresses the correctness of the {\isa{gcd}} 
@@ -1495,7 +1495,7 @@
 most fundamental type of proof.  Backward proof, by working  from goals to
 subgoals, can help us find a difficult proof.  But it is
 not always the best way of presenting the proof so found.  Forward
-proof is particuarly good for reasoning from the general
+proof is particularly good for reasoning from the general
 to the specific.  For example, consider the following distributive law for
 the 
 \isa{gcd} function:
@@ -1610,11 +1610,11 @@
 \isa{rule} method whose operand is expressed using forward reasoning:
 \begin{isabelle}
 \isacommand{lemma}\ gcd_mult\
-[simp]{:}\
+[simp]:\
 "gcd(k,\
 k{\isacharasterisk}n)\ =\
 k"\isanewline
-\isacommand{apply}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]{)}\isanewline
+\isacommand{apply}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])\isanewline
 \isacommand{done}
 \end{isabelle}
 Compared with the previous proof of \isa{gcd_mult}, this
@@ -1625,11 +1625,8 @@
 At the start  of this section, we also saw a proof of $\gcd(k,k)=k$.  Here
 is the Isabelle version: 
 \begin{isabelle}
-\isacommand{lemma}\ gcd_self\
-[simp]{:}\
-"gcd(k{,}k)\
-=\ k"\isanewline
-\isacommand{apply}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified]{)}\isanewline
+\isacommand{lemma}\ gcd_self\ [simp]:\ "gcd(k,k)\ =\ k"\isanewline
+\isacommand{apply}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])\isanewline
 \isacommand{done}
 \end{isabelle}
 
@@ -1646,7 +1643,7 @@
 prove an instance of its first premise:
 \begin{isabelle}
 \isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline
-\isacommand{apply}\ (simp\ add:\ gcd{.}simps)\isanewline
+\isacommand{apply}\ (simp\ add:\ gcd.simps)\isanewline
 \isacommand{done}%
 \end{isabelle}
 We have evaluated an application of the \isa{gcd} function by
@@ -1779,13 +1776,13 @@
 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{\isacharasterisk}n)\ div\ n\ =\ (m::nat)"\isanewline
+\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m{\isacharasterisk}n"\ n])\isanewline
 \isacommand{apply}\ (simp)\isanewline
 \isacommand{done}
 \end{isabelle}
 The first step inserts the law, specifying \isa{m*n} and
-\isa{n} for its variables.  Notice that nontrivial expressions must be
+\isa{n} for its variables.  Notice that non-trivial expressions must be
 enclosed in quotation marks.  Here is the resulting 
 subgoal, with its new assumption: 
 \begin{isabelle}