# HG changeset patch
# User paulson
# Date 1005558998 -3600
# Node ID d2758965362ece433d6aaafdc8c38016dae9be25
# Parent  13c5469b4bb38764423e595178f79823c9353912
new-style numerals without leading #, along with generic 0 and 1

diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Inductive/Advanced.thy
--- a/doc-src/TutorialI/Inductive/Advanced.thy	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Advanced.thy	Mon Nov 12 10:56:38 2001 +0100
@@ -76,6 +76,7 @@
 by (blast intro!: mono_Int monoI gterms_mono)
 
 
+text{*the following declaration isn't actually used*}
 consts integer_arity :: "integer_op \<Rightarrow> nat"
 primrec
 "integer_arity (Number n)        = 0"
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Inductive/document/Advanced.tex
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex	Mon Nov 12 10:56:38 2001 +0100
@@ -112,10 +112,12 @@
 \isacommand{lemma}\ gterms{\isacharunderscore}Int{\isacharunderscore}eq\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ \ \ \ {\isachardoublequote}gterms\ {\isacharparenleft}F{\isasyminter}G{\isacharparenright}\ {\isacharequal}\ gterms\ F\ {\isasyminter}\ gterms\ G{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isanewline
-\isanewline
-\isanewline
-\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ mono{\isacharunderscore}Int\ monoI\ gterms{\isacharunderscore}mono{\isacharparenright}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+the following declaration isn't actually used%
+\end{isamarkuptext}%
+\isamarkuptrue%
 \isacommand{consts}\ integer{\isacharunderscore}arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}integer{\isacharunderscore}op\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{primrec}\isanewline
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy	Mon Nov 12 10:56:38 2001 +0100
@@ -33,15 +33,6 @@
 as far as HERE.
 *}
 
-
-text {*
-@{thm[display] gcd_1}
-\rulename{gcd_1}
-
-@{thm[display] gcd_1_left}
-\rulename{gcd_1_left}
-*};
-
 text{*\noindent
 SKIP THIS PROOF
 *}
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Mon Nov 12 10:56:38 2001 +0100
@@ -1818,7 +1818,7 @@
 appearance from left to right.  In this case, the variables  are \isa{?k}, \isa{?m}
 and~\isa{?n}. So, the expression
 \hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m}
-by~\isa{1}.\REMARK{which 1 do we use?? (right the way down)}
+by~\isa{1}.
 \begin{isabelle}
 \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1]
 \end{isabelle}
@@ -1890,8 +1890,7 @@
 \end{isabelle}
 %
 Normally we would never name the intermediate theorems
-such as \isa{gcd_mult_0} and
-\isa{gcd_mult_1} but would combine
+such as \isa{gcd_mult_0} and \isa{gcd_mult_1} but would combine
 the three forward steps: 
 \begin{isabelle}
 \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]%
@@ -1959,7 +1958,7 @@
 First, we
 prove an instance of its first premise:
 \begin{isabelle}
-\isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline
+\isacommand{lemma}\ relprime_20_81:\ "gcd(20,81)\ =\ 1"\isanewline
 \isacommand{by}\ (simp\ add:\ gcd.simps)
 \end{isabelle}
 We have evaluated an application of the \isa{gcd} function by
@@ -1973,7 +1972,7 @@
 \end{isabelle}
 yields the theorem
 \begin{isabelle}
-\ \ \ \ \ \#20\ dvd\ (?m\ *\ \#81)\ \isasymLongrightarrow\ \#20\ dvd\ ?m%
+\ \ \ \ \ 20\ dvd\ (?m\ *\ 81)\ \isasymLongrightarrow\ 20\ dvd\ ?m%
 \end{isabelle}
 %
 \isa{OF} takes any number of operands.  Consider 
@@ -2048,10 +2047,10 @@
 
 For example, let us prove a fact about divisibility in the natural numbers:
 \begin{isabelle}
-\isacommand{lemma}\ "\#2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
+\isacommand{lemma}\ "2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq
 \ Suc(u*n)"\isanewline
 \isacommand{apply}\ intro\isanewline
-\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
+\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False%
 \end{isabelle}
 %
 The key step is to apply the function \ldots\isa{mod\ u} to both sides of the
@@ -2060,7 +2059,7 @@
 \begin{isabelle}
 \isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\
 arg_cong)\isanewline
-\ 1.\ \isasymlbrakk \#2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
+\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\
 u\isasymrbrakk \ \isasymLongrightarrow \ False
 \end{isabelle}
 %
@@ -2175,13 +2174,13 @@
 
 Look at the following example. 
 \begin{isabelle}
-\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ \#37;\ \#66\ <\ \#2*z;\ z*z\
-\isasymnoteq\ \#1225;\ Q(\#34);\ Q(\#36)\isasymrbrakk\isanewline
+\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ 37;\ 66\ <\ 2*z;\ z*z\
+\isasymnoteq\ 1225;\ Q(34);\ Q(36)\isasymrbrakk\isanewline
 \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline
-\isacommand{apply}\ (subgoal_tac\ "z\ =\ \#34\ \isasymor\ z\ =\
-\#36")\isanewline
+\isacommand{apply}\ (subgoal_tac\ "z\ =\ 34\ \isasymor\ z\ =\
+36")\isanewline
 \isacommand{apply}\ blast\isanewline
-\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ \#35")\isanewline
+\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ 35")\isanewline
 \isacommand{apply}\ arith\isanewline
 \isacommand{apply}\ force\isanewline
 \isacommand{done}
@@ -2196,25 +2195,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;\
-%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
-\ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline
+%\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
+\ \ \ \ \ 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
-\ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36
+\ 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 (\isa{blast}), but for the second Isabelle needs help to eliminate
 the case
 \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\
-\#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
-\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35
+\ 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
+\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ 35
 \end{isabelle}
 
 Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic
@@ -2286,8 +2285,8 @@
 implications in which most of the antecedents are proved by assumption, but one is
 proved by arithmetic:
 \begin{isabelle}
-\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<\#5\isasymlongrightarrow P;\
-Suc\ x\ <\ \#5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
+\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<5\isasymlongrightarrow P;\
+Suc\ x\ <\ 5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline
 \isacommand{by}\ (drule\ mp,\ (assumption|arith))+
 \end{isabelle}
 The \isa{arith}
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Nov 12 10:56:38 2001 +0100
@@ -83,8 +83,15 @@
 *}
 
 
+lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
+apply (clarsimp split: nat_diff_split)
+ --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (subgoal_tac "n=0", force, arith)
+done
+
+
 lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
-apply (clarsimp split: nat_diff_split)
+apply (simp split: nat_diff_split, clarify)
  --{* @{subgoals[display,indent=0,margin=65]} *}
 apply (subgoal_tac "n=0 | n=1", force, arith)
 done
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Types/Records.thy
--- a/doc-src/TutorialI/Types/Records.thy	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/Records.thy	Mon Nov 12 10:56:38 2001 +0100
@@ -112,7 +112,6 @@
   @{text [display]
 "    point = (| Xcoord :: int, Ycoord :: int |)
     'a point_scheme = (| Xcoord :: int, Ycoord :: int, ... :: 'a |)"}
-  Extensions `...' must be in type class @{text more}.
 *}
 
 constdefs
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Nov 12 10:56:38 2001 +0100
@@ -130,9 +130,25 @@
 \rulename{nat_diff_split}%
 \end{isamarkuptext}%
 \isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
+\ %
+\isamarkupcmt{\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
+\end{isabelle}%
+}
+\isanewline
+\isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}n{\isacharequal}{\isadigit{0}}{\isachardoublequote}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{done}\isanewline
+\isanewline
+\isanewline
+\isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
-\isacommand{apply}\ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline
+\isacommand{apply}\ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline
 \ %
 \isamarkupcmt{\begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex	Mon Nov 12 10:56:38 2001 +0100
@@ -41,15 +41,15 @@
 \label{sec:numerals}
 
 \index{numeric literals|(}%
-Literals are available for the types of natural numbers, integers 
-and reals and denote integer values of arbitrary size. 
-They begin 
-with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and 
-then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3} 
-and \isa{\#441223334678}.\REMARK{will need updating?}
+The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
+respectively, for all numeric types.  Other values are expressed by numeric
+literals, which consist of one or more decimal digits optionally preceeded by
+a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
+\isa{441223334678}.  Literals are available for the types of natural numbers,
+integers and reals; they denote integer values of arbitrary size.
 
 Literals look like constants, but they abbreviate 
-terms, representing the number in a two's complement binary notation. 
+terms representing the number in a two's complement binary notation. 
 Isabelle performs arithmetic on literals by rewriting rather 
 than using the hardware arithmetic. In most cases arithmetic 
 is fast enough, even for large numbers. The arithmetic operations 
@@ -64,14 +64,14 @@
 type constraints.  Here is an example of what can go wrong:
 \par
 \begin{isabelle}
-\isacommand{lemma}\ "\#2\ *\ m\ =\ m\ +\ m"
+\isacommand{lemma}\ "2\ *\ m\ =\ m\ +\ m"
 \end{isabelle}
 %
 Carefully observe how Isabelle displays the subgoal:
 \begin{isabelle}
-\ 1.\ (\#2::'a)\ *\ m\ =\ m\ +\ m
+\ 1.\ (2::'a)\ *\ m\ =\ m\ +\ m
 \end{isabelle}
-The type \isa{'a} given for the literal \isa{\#2} warns us that no numeric
+The type \isa{'a} given for the literal \isa{2} warns us that no numeric
 type has been specified.  The problem is underspecified.  Given a type
 constraint such as \isa{nat}, \isa{int} or \isa{real}, it becomes trivial.
 \end{warn}
@@ -83,13 +83,13 @@
 rejected:
 \begin{isabelle}
 \isacommand{recdef}\ h\ "\isacharbraceleft \isacharbraceright "\isanewline
-"h\ \#3\ =\ \#2"\isanewline
+"h\ 3\ =\ 2"\isanewline
 "h\ i\ \ =\ i"
 \end{isabelle}
 
 You should use a conditional expression instead:
 \begin{isabelle}
-"h\ i\ =\ (if\ i\ =\ \#3\ then\ \#2\ else\ i)"
+"h\ i\ =\ (if\ i\ =\ 3\ then\ 2\ else\ i)"
 \end{isabelle}
 \index{numeric literals|)}
 \end{warn}
@@ -106,29 +106,30 @@
 
 \subsubsection{Literals}
 \index{numeric literals!for type \protect\isa{nat}}%
-The notational options for the natural numbers are confusing.  The 
-constant \cdx{0} is overloaded to serve as the neutral value 
-in a variety of additive types. The symbols \sdx{1} and \sdx{2} are 
-not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
-respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are
-syntactically different from \isa{0}, \isa{1} and \isa{2}. You  will\REMARK{will need updating?}
-sometimes prefer one notation to the other. Literals are  obviously
-necessary to express large values, while \isa{0} and \isa{Suc}  are needed
-in order to match many theorems, including the rewrite  rules for primitive
-recursive functions. The following default  simplification rules replace
+The notational options for the natural  numbers are confusing.  Recall that an
+overloaded constant can be defined independently for each type; the definition
+of \cdx{1} for type \isa{nat} is
+\begin{isabelle}
+1\ \isasymequiv\ Suc\ 0
+\rulename{One_nat_def}
+\end{isabelle}
+This is installed as a simplification rule, so the simplifier will replace
+every occurrence of \isa{1::nat} by \isa{Suc\ 0}.  Literals are obviously
+better than nested \isa{Suc}s at expressing large values.  But many theorems,
+including the rewrite rules for primitive recursive functions, can only be
+applied to terms of the form \isa{Suc\ $n$}.
+
+The following default  simplification rules replace
 small literals by zero and successor: 
 \begin{isabelle}
-\#0\ =\ 0
-\rulename{numeral_0_eq_0}\isanewline
-\#1\ =\ 1
-\rulename{numeral_1_eq_1}\isanewline
-\#2\ +\ n\ =\ Suc\ (Suc\ n)
+2\ +\ n\ =\ Suc\ (Suc\ n)
 \rulename{add_2_eq_Suc}\isanewline
-n\ +\ \#2\ =\ Suc\ (Suc\ n)
+n\ +\ 2\ =\ Suc\ (Suc\ n)
 \rulename{add_2_eq_Suc'}
 \end{isabelle}
-In special circumstances, you may wish to remove or reorient 
-these rules. 
+It is less easy to transform \isa{100} into \isa{Suc\ 99} (for example), and
+the simplifier will normally reverse this transformation.  Novices should
+express natural numbers using \isa{0} and \isa{Suc} only.
 
 \subsubsection{Typical lemmas}
 Inequalities involving addition and subtraction alone can be proved
@@ -225,11 +226,17 @@
 d))
 \rulename{nat_diff_split}
 \end{isabelle}
-For example, this splitting proves the following fact, which lies outside the scope of
-linear arithmetic:\REMARK{replace by new example!}
+For example, splitting helps to prove the following fact:
 \begin{isabelle}
-\isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
-\isacommand{apply}\ (simp\ split:\ nat_diff_split)\isanewline
+\isacommand{lemma}\ "(n\ -\ 2)\ *\ (n\ +\ 2)\ =\ n\ *\ n\ -\ (4::nat)"\isanewline
+\isacommand{apply}\ (simp\ split:\ nat_diff_split,\ clarify)\isanewline
+\ 1.\ \isasymAnd d.\ \isasymlbrakk n\ <\ 2;\ n\ *\ n\ =\ 4\ +\ d\isasymrbrakk \ \isasymLongrightarrow \ d\ =\ 0
+\end{isabelle}
+The result lies outside the scope of linear arithmetic, but
+ it is easily found
+if we explicitly split \isa{n<2} as \isa{n=0} or \isa{n=1}:
+\begin{isabelle}
+\isacommand{apply}\ (subgoal_tac\ "n=0\ |\ n=1",\ force,\ arith)\isanewline
 \isacommand{done}
 \end{isabelle}
 
@@ -313,13 +320,13 @@
 mathematical practice: the sign of the remainder follows that
 of the divisor:
 \begin{isabelle}
-\#0\ <\ b\ \isasymLongrightarrow \ \#0\ \isasymle \ a\ mod\ b%
+0\ <\ b\ \isasymLongrightarrow \ 0\ \isasymle \ a\ mod\ b%
 \rulename{pos_mod_sign}\isanewline
-\#0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
+0\ <\ b\ \isasymLongrightarrow \ a\ mod\ b\ <\ b%
 \rulename{pos_mod_bound}\isanewline
-b\ <\ \#0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ \#0
+b\ <\ 0\ \isasymLongrightarrow \ a\ mod\ b\ \isasymle \ 0
 \rulename{neg_mod_sign}\isanewline
-b\ <\ \#0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
+b\ <\ 0\ \isasymLongrightarrow \ b\ <\ a\ mod\ b%
 \rulename{neg_mod_bound}
 \end{isabelle}
 ML treats negative divisors in the same way, but most computer hardware
@@ -342,9 +349,9 @@
 \end{isabelle}
 
 \begin{isabelle}
-\#0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
+0\ <\ c\ \isasymLongrightarrow \ a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
 \rulename{zdiv_zmult2_eq}\isanewline
-\#0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
+0\ <\ c\ \isasymLongrightarrow \ a\ mod\ (b*c)\ =\ b*(a\ div\ b\ mod\
 c)\ +\ a\ mod\ b%
 \rulename{zmod_zmult2_eq}
 \end{isabelle}
@@ -426,18 +433,18 @@
 \isa{int} and only express integral values.  Fractions expressed
 using the division operator are automatically simplified to lowest terms:
 \begin{isabelle}
-\ 1.\ P\ ((\#3\ /\ \#4)\ *\ (\#8\ /\ \#15))\isanewline
+\ 1.\ P\ ((3\ /\ 4)\ *\ (8\ /\ 15))\isanewline
 \isacommand{apply} simp\isanewline
-\ 1.\ P\ (\#2\ /\ \#5)
+\ 1.\ P\ (2\ /\ 5)
 \end{isabelle}
 Exponentiation can express floating-point values such as
-\isa{\#2 * \#10\isacharcircum\#6}, but at present no special simplification
+\isa{2 * 10\isacharcircum6}, but at present no special simplification
 is performed.
 
 
 \begin{warn}
 Type \isa{real} is only available in the logic HOL-Real, which
-is  HOL extended with the rather substantial development of the real
+is  HOL extended with a definitional development of the real
 numbers.  Base your theory upon theory
 \thydx{Real}, not the usual \isa{Main}.%
 \index{real numbers|)}\index{*real (type)|)}
diff -r 13c5469b4bb3 -r d2758965362e doc-src/TutorialI/Types/records.tex
--- a/doc-src/TutorialI/Types/records.tex	Mon Nov 12 10:44:55 2001 +0100
+++ b/doc-src/TutorialI/Types/records.tex	Mon Nov 12 10:56:38 2001 +0100
@@ -36,7 +36,7 @@
 \isa{point}:
 \begin{isabelle}
 \isacommand{constdefs}\ \ \ pt1\ ::\ point\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ \#999,\ Ycoord\ =\ \#23\ |)"
+\ \ \ \ \ \ \ \ \ \ \ \ "pt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23\ |)"
 \end{isabelle}
 We see above the ASCII notation for record brackets.  You can also use
 the symbolic brackets \isa{\isasymlparr} and  \isa{\isasymrparr}.
@@ -45,7 +45,7 @@
 \begin{isabelle}
 \isacommand{constdefs}\ \ \ pt2\ ::\ "(|\ Xcoord\ ::\ int,\ Ycoord\ ::\ int\
 |)"\ \isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ \#-45,\ Ycoord\ =\ \#97\ |)"
+\ \ \ \ \ \ \ \ \ \ \ \ "pt2\ ==\ (|\ Xcoord\ =\ -45,\ Ycoord\ =\ 97\ |)"
 \end{isabelle}
 
 For each field, there is a \emph{selector} function of the same name.  For
@@ -57,12 +57,12 @@
 \isacommand{by}\ simp
 \end{isabelle}
 The \emph{update} operation is functional.  For example,
-\isa{p\isasymlparr Xcoord:=\#0\isasymrparr} is a record whose \isa{Xcoord} value
+\isa{p\isasymlparr Xcoord:=0\isasymrparr} is a record whose \isa{Xcoord} value
 is zero and whose
 \isa{Ycoord} value is copied from~\isa{p}.  Updates are also simplified
 automatically:
 \begin{isabelle}
-\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ \#0\ |)\
+\isacommand{lemma}\ "(|\ Xcoord\ =\ a,\ Ycoord\ =\ b\ |)\ (|\ Xcoord:=\ 0\ |)\
 =\isanewline
 \ \ \ \ \ \ \ \ (|\ Xcoord\ =\ 0,\ Ycoord\ =\ b\ |)"\isanewline
 \isacommand{by}\ simp
@@ -94,7 +94,7 @@
 order:
 \begin{isabelle}
 \isacommand{constdefs}\ \ \ cpt1\ ::\ cpoint\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ \#999,\ Ycoord\ =\ \#23,\ col\
+\ \ \ \ \ \ \ \ \ \ \ \ "cpt1\ ==\ (|\ Xcoord\ =\ 999,\ Ycoord\ =\ 23,\ col\
 =\ Green\ |)"
 \end{isabelle}
 
@@ -141,14 +141,11 @@
 comprises all possible extensions to those two fields.  For example,
 let us define two operations --- methods, if we regard records as
 objects --- to get and set any point's
-\isa{Xcoord} field.  The sort constraint in \isa{'a::more} is
-required, since all extensions must belong to the type class
-\isa{more}.%
-\REMARK{Why, and what does this imply in practice?}
+\isa{Xcoord} field. 
 \begin{isabelle}
-\ \ getX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ int"\isanewline
+\ \ getX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ int"\isanewline
 \ \ \ "getX\ r\ ==\ Xcoord\ r"\isanewline
-\ \ setX\ ::\ "[('a::more)\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
+\ \ setX\ ::\ "['a\ point_scheme,\ int]\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
 \ \ \ "setX\ r\ a\ ==\ r\ (|\ Xcoord\ :=\ a\ |)"
 \end{isabelle}
 
@@ -158,9 +155,8 @@
 extensions, such as \isa{cpoint}:
 \begin{isabelle}
 \isacommand{constdefs}\isanewline
-\ \ incX\ ::\ "('a::more)\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
-\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\
-\#1,\isanewline
+\ \ incX\ ::\ "'a\ point_scheme\ \isasymRightarrow \ 'a\ point_scheme"\isanewline
+\ \ "incX\ r\ ==\ \isasymlparr Xcoord\ =\ (Xcoord\ r)\ +\ 1,\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ Ycoord\ =\ Ycoord\ r,\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymdots \ =\ point.more\
 r\isasymrparr"
@@ -169,7 +165,7 @@
 Generic theorems can be proved about generic methods.  This trivial
 lemma relates \isa{incX} to \isa{getX} and \isa{setX}:
 \begin{isabelle}
-\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ \#1)"\isanewline
+\isacommand{lemma}\ "incX\ r\ =\ setX\ r\ ((getX\ r)\ +\ 1)"\isanewline
 \isacommand{by}\ (simp\ add:\ getX_def\ setX_def\ incX_def)
 \end{isabelle}