Changed part of the examples to int.

--- a/doc-src/Locales/Locales/Examples1.thy	Thu Oct 15 22:07:18 2009 +0200
+++ b/doc-src/Locales/Locales/Examples1.thy	Thu Oct 15 22:22:08 2009 +0200
@@ -18,8 +18,8 @@
   interpretations in proofs, in
   Section~\ref{sec:local-interpretation}.
 
-  As an example, consider the type of natural numbers @{typ nat}.  The
-  relation @{term "op \<le>"} is a total order over @{typ nat},
+  As an example, consider the type of integers @{typ int}.  The
+  relation @{term "op \<le>"} is a total order over @{typ int},
   divisibility @{text "op dvd"} forms a distributive lattice.  We start with the
   interpretation that @{term "op \<le>"} is a partial order.  The facilities of
   the interpretation command are explored gradually in three versions.
@@ -32,15 +32,15 @@
 text {*
   The command \isakeyword{interpretation} is for the interpretation of
   locale in theories.  In the following example, the parameter of locale
-  @{text partial_order} is replaced by @{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow>
+  @{text partial_order} is replaced by @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow>
   bool"} and the locale instance is interpreted in the current
   theory. *}
 
-  interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
 txt {* \normalsize
   The argument of the command is a simple \emph{locale expression}
   consisting of the name of the interpreted locale, which is
-  preceded by the qualifier @{text "nat:"} and succeeded by a
+  preceded by the qualifier @{text "int:"} and succeeded by a
   white-space-separated list of terms, which provide a full
   instantiation of the locale parameters.  The parameters are referred
   to by order of declaration, which is also the order in which
@@ -56,9 +56,9 @@
 text {*  The effect of the command is that instances of all
   conclusions of the locale are available in the theory, where names
   are prefixed by the qualifier.  For example, transitivity for @{typ
-  nat} is named @{thm [source] nat.trans} and is the following
+  int} is named @{thm [source] int.trans} and is the following
   theorem:
-  @{thm [display, indent=2] nat.trans}
+  @{thm [display, indent=2] int.trans}
   It is not possible to reference this theorem simply as @{text
   trans}, which prevents unwanted hiding of existing theorems of the
   theory by an interpretation. *}
@@ -67,20 +67,20 @@
 subsection {* Second Version: Replacement of Definitions *}
 
 text {* Not only does the above interpretation qualify theorem names.
-  The prefix @{text nat} is applied to all names introduced in locale
+  The prefix @{text int} is applied to all names introduced in locale
   conclusions including names introduced in definitions.  The
-  qualified name @{text nat.less} refers to
-  the interpretation of the definition, which is @{term nat.less}.
+  qualified name @{text int.less} refers to
+  the interpretation of the definition, which is @{term int.less}.
   Qualified name and expanded form may be used almost
   interchangeably.%
-\footnote{Since @{term "op \<le>"} is polymorphic, for @{term nat.less} a
-  more general type will be inferred than for @{text nat.less} which
-  is over type @{typ nat}.}
+\footnote{Since @{term "op \<le>"} is polymorphic, for @{term int.less} a
+  more general type will be inferred than for @{text int.less} which
+  is over type @{typ int}.}
   The latter is preferred on output, as for example in the theorem
-  @{thm [source] nat.less_le_trans}: @{thm [display, indent=2]
-  nat.less_le_trans}
+  @{thm [source] int.less_le_trans}: @{thm [display, indent=2]
+  int.less_le_trans}
   Both notations for the strict order are not satisfactory.  The
-  constant @{term "op <"} is the strict order for @{typ nat}.
+  constant @{term "op <"} is the strict order for @{typ int}.
   In order to allow for the desired replacement, interpretation
   accepts \emph{equations} in addition to the parameter instantiation.
   These follow the locale expression and are indicated with the

--- a/doc-src/Locales/Locales/Examples2.thy	Thu Oct 15 22:07:18 2009 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy	Thu Oct 15 22:22:08 2009 +0200
@@ -2,16 +2,16 @@
 imports Examples
 begin
 text {* \vspace{-5ex} *}
-  interpretation %visible nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool"
-    where "partial_order.less op \<le> (x::nat) y = (x < y)"
+  interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
+    where "partial_order.less op \<le> (x::int) y = (x < y)"
   proof -
     txt {* \normalsize The goals are @{subgoals [display]}
       The proof that @{text \<le>} is a partial order is as above. *}
-    show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+    show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
       by unfold_locales auto
     txt {* \normalsize The second goal is shown by unfolding the
       definition of @{term "partial_order.less"}. *}
-    show "partial_order.less op \<le> (x::nat) y = (x < y)"
+    show "partial_order.less op \<le> (x::int) y = (x < y)"
       unfolding partial_order.less_def [OF `partial_order op \<le>`]
       by auto
   qed

--- a/doc-src/Locales/Locales/Examples3.thy	Thu Oct 15 22:07:18 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy	Thu Oct 15 22:22:08 2009 +0200
@@ -8,7 +8,7 @@
   \label{sec:local-interpretation} *}
 
 text {* In the above example, the fact that @{term "op \<le>"} is a partial
-  order for the natural numbers was used in the second goal to
+  order for the integers was used in the second goal to
   discharge the premise in the definition of @{text "op \<sqsubset>"}.  In
   general, proofs of the equations not only may involve definitions
   fromthe interpreted locale but arbitrarily complex arguments in the
@@ -18,21 +18,21 @@
   The command for local interpretations is \isakeyword{interpret}.  We
   repeat the example from the previous section to illustrate this. *}
 
-  interpretation %visible nat: partial_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-    where "partial_order.less op \<le> (x::nat) y = (x < y)"
+  interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
+    where "partial_order.less op \<le> (x::int) y = (x < y)"
   proof -
-    show "partial_order (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+    show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
       by unfold_locales auto
-    then interpret nat: partial_order "op \<le> :: [nat, nat] \<Rightarrow> bool" .
-    show "partial_order.less op \<le> (x::nat) y = (x < y)"
-      unfolding nat.less_def by auto
+    then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
+    show "partial_order.less op \<le> (x::int) y = (x < y)"
+      unfolding int.less_def by auto
   qed
 
 text {* The inner interpretation is immediate from the preceding fact
   and proved by assumption (Isar short hand ``.'').  It enriches the
   local proof context by the theorems
   also obtained in the interpretation from Section~\ref{sec:po-first},
-  and @{text nat.less_def} may directly be used to unfold the
+  and @{text int.less_def} may directly be used to unfold the
   definition.  Theorems from the local interpretation disappear after
   leaving the proof context --- that is, after the closing a
   \isakeyword{next} or \isakeyword{qed} statement. *}
@@ -42,23 +42,23 @@
 
 text {* Further interpretations are necessary for
   the other locales.  In @{text lattice} the operations @{text \<sqinter>} and
-  @{text \<squnion>} are substituted by @{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} and
-  @{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"}.  The entire proof for the
+  @{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"} and
+  @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}.  The entire proof for the
   interpretation is reproduced to give an example of a more
   elaborate interpretation proof.  *}
 
-  interpretation %visible nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
-    where "lattice.meet op \<le> (x::nat) y = min x y"
-      and "lattice.join op \<le> (x::nat) y = max x y"
+  interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
+    where "lattice.meet op \<le> (x::int) y = min x y"
+      and "lattice.join op \<le> (x::int) y = max x y"
   proof -
-    show "lattice (op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool)"
+    show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
       txt {* \normalsize We have already shown that this is a partial
 	order, *}
       apply unfold_locales
       txt {* \normalsize hence only the lattice axioms remain to be
 	shown: @{subgoals [display]}  After unfolding @{text is_inf} and
 	@{text is_sup}, *}
-      apply (unfold nat.is_inf_def nat.is_sup_def)
+      apply (unfold int.is_inf_def int.is_sup_def)
       txt {* \normalsize the goals become @{subgoals [display]}
 	This can be solved by Presburger arithmetic, which is contained
 	in @{text arith}. *}
@@ -66,40 +66,40 @@
     txt {* \normalsize In order to show the equations, we put ourselves
       in a situation where the lattice theorems can be used in a
       convenient way. *}
-    then interpret nat: lattice "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool" .
-    show "lattice.meet op \<le> (x::nat) y = min x y"
-      by (bestsimp simp: nat.meet_def nat.is_inf_def)
-    show "lattice.join op \<le> (x::nat) y = max x y"
-      by (bestsimp simp: nat.join_def nat.is_sup_def)
+    then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
+    show "lattice.meet op \<le> (x::int) y = min x y"
+      by (bestsimp simp: int.meet_def int.is_inf_def)
+    show "lattice.join op \<le> (x::int) y = max x y"
+      by (bestsimp simp: int.join_def int.is_sup_def)
   qed
 
 text {* Next follows that @{text "op \<le>"} is a total order, again for
-  the natural numbers. *}
+  the integers. *}
 
-  interpretation %visible nat: total_order "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"
+  interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
     by unfold_locales arith
 
 text {* Theorems that are available in the theory at this point are shown in
-  Table~\ref{tab:nat-lattice}.  Two points are worth noting:
+  Table~\ref{tab:int-lattice}.  Two points are worth noting:
 
 \begin{table}
 \hrule
 \vspace{2ex}
 \begin{center}
 \begin{tabular}{l}
-  @{thm [source] nat.less_def} from locale @{text partial_order}: \\
-  \quad @{thm nat.less_def} \\
-  @{thm [source] nat.meet_left} from locale @{text lattice}: \\
-  \quad @{thm nat.meet_left} \\
-  @{thm [source] nat.join_distr} from locale @{text distrib_lattice}: \\
-  \quad @{thm nat.join_distr} \\
-  @{thm [source] nat.less_total} from locale @{text total_order}: \\
-  \quad @{thm nat.less_total}
+  @{thm [source] int.less_def} from locale @{text partial_order}: \\
+  \quad @{thm int.less_def} \\
+  @{thm [source] int.meet_left} from locale @{text lattice}: \\
+  \quad @{thm int.meet_left} \\
+  @{thm [source] int.join_distr} from locale @{text distrib_lattice}: \\
+  \quad @{thm int.join_distr} \\
+  @{thm [source] int.less_total} from locale @{text total_order}: \\
+  \quad @{thm int.less_total}
 \end{tabular}
 \end{center}
 \hrule
-\caption{Interpreted theorems for @{text \<le>} on the natural numbers.}
-\label{tab:nat-lattice}
+\caption{Interpreted theorems for @{text \<le>} on the integers.}
+\label{tab:int-lattice}
 \end{table}
 
 \begin{itemize}
@@ -112,7 +112,7 @@
   up in the hierarchy, regardless whether imported or proved via the
   \isakeyword{sublocale} command.
 \item
-  Theorem @{thm [source] nat.less_total} makes use of @{term "op <"}
+  Theorem @{thm [source] int.less_total} makes use of @{term "op <"}
   although an equation for the replacement of @{text "op \<sqsubset>"} was only
   given in the interpretation of @{text partial_order}.  These
   equations are pushed downwards the hierarchy for related
@@ -229,7 +229,7 @@
   For example, \isakeyword{print\_interps} @{term partial_order}
   outputs the following:
 \begin{alltt}
-  nat! : partial_order "op \(\le\)"
+  int! : partial_order "op \(\le\)"
   nat_dvd! : partial_order "op dvd"
 \end{alltt}
   The interpretation qualifiers on the left are decorated with an

--- a/doc-src/Locales/Locales/document/Examples1.tex	Thu Oct 15 22:07:18 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples1.tex	Thu Oct 15 22:22:08 2009 +0200
@@ -36,8 +36,8 @@
   interpretations in proofs, in
   Section~\ref{sec:local-interpretation}.
 
-  As an example, consider the type of natural numbers \isa{nat}.  The
-  relation \isa{op\ {\isasymle}} is a total order over \isa{nat},
+  As an example, consider the type of integers \isa{int}.  The
+  relation \isa{op\ {\isasymle}} is a total order over \isa{int},
   divisibility \isa{op\ dvd} forms a distributive lattice.  We start with the
   interpretation that \isa{op\ {\isasymle}} is a partial order.  The facilities of
   the interpretation command are explored gradually in three versions.%
@@ -63,12 +63,12 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
+\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}%
 \begin{isamarkuptxt}%
 \normalsize
   The argument of the command is a simple \emph{locale expression}
   consisting of the name of the interpreted locale, which is
-  preceded by the qualifier \isa{nat{\isacharcolon}} and succeeded by a
+  preceded by the qualifier \isa{int{\isacharcolon}} and succeeded by a
   white-space-separated list of terms, which provide a full
   instantiation of the locale parameters.  The parameters are referred
   to by order of declaration, which is also the order in which
@@ -94,7 +94,7 @@
 \begin{isamarkuptext}%
 The effect of the command is that instances of all
   conclusions of the locale are available in the theory, where names
-  are prefixed by the qualifier.  For example, transitivity for \isa{nat} is named \isa{nat{\isachardot}trans} and is the following
+  are prefixed by the qualifier.  For example, transitivity for \isa{int} is named \isa{int{\isachardot}trans} and is the following
   theorem:
   \begin{isabelle}%
 \ \ {\isasymlbrakk}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymle}\ {\isacharquery}z%
@@ -110,22 +110,22 @@
 %
 \begin{isamarkuptext}%
 Not only does the above interpretation qualify theorem names.
-  The prefix \isa{nat} is applied to all names introduced in locale
+  The prefix \isa{int} is applied to all names introduced in locale
   conclusions including names introduced in definitions.  The
-  qualified name \isa{nat{\isachardot}less} refers to
+  qualified name \isa{int{\isachardot}less} refers to
   the interpretation of the definition, which is \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}}.
   Qualified name and expanded form may be used almost
   interchangeably.%
 \footnote{Since \isa{op\ {\isasymle}} is polymorphic, for \isa{partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}} a
-  more general type will be inferred than for \isa{nat{\isachardot}less} which
-  is over type \isa{nat}.}
+  more general type will be inferred than for \isa{int{\isachardot}less} which
+  is over type \isa{int}.}
   The latter is preferred on output, as for example in the theorem
-  \isa{nat{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
+  \isa{int{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}%
 \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}z{\isasymrbrakk}\isanewline
 \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharquery}x\ {\isacharquery}z%
 \end{isabelle}
   Both notations for the strict order are not satisfactory.  The
-  constant \isa{op\ {\isacharless}} is the strict order for \isa{nat}.
+  constant \isa{op\ {\isacharless}} is the strict order for \isa{int}.
   In order to allow for the desired replacement, interpretation
   accepts \emph{equations} in addition to the parameter instantiation.
   These follow the locale expression and are indicated with the

--- a/doc-src/Locales/Locales/document/Examples2.tex	Thu Oct 15 22:07:18 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples2.tex	Thu Oct 15 22:22:08 2009 +0200
@@ -29,8 +29,8 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}int{\isacharcomma}\ int{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}%
 \begin{isamarkuptxt}%
@@ -42,7 +42,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ auto%
 \begin{isamarkuptxt}%
@@ -51,7 +51,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
 \ partial{\isacharunderscore}order{\isachardot}less{\isacharunderscore}def\ {\isacharbrackleft}OF\ {\isacharbackquoteopen}partial{\isacharunderscore}order\ op\ {\isasymle}{\isacharbackquoteclose}{\isacharbrackright}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%

--- a/doc-src/Locales/Locales/document/Examples3.tex	Thu Oct 15 22:07:18 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Thu Oct 15 22:22:08 2009 +0200
@@ -45,7 +45,7 @@
 %
 \begin{isamarkuptext}%
 In the above example, the fact that \isa{op\ {\isasymle}} is a partial
-  order for the natural numbers was used in the second goal to
+  order for the integers was used in the second goal to
   discharge the premise in the definition of \isa{op\ {\isasymsqsubset}}.  In
   general, proofs of the equations not only may involve definitions
   fromthe interpreted locale but arbitrarily complex arguments in the
@@ -63,22 +63,22 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ auto\isanewline
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}nat{\isacharcomma}\ nat{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ int{\isacharcolon}\ partial{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ {\isacharbrackleft}int{\isacharcomma}\ int{\isacharbrackright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ nat{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ int{\isachardot}less{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
 \ auto\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 %
@@ -94,7 +94,7 @@
   and proved by assumption (Isar short hand ``.'').  It enriches the
   local proof context by the theorems
   also obtained in the interpretation from Section~\ref{sec:po-first},
-  and \isa{nat{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the
+  and \isa{int{\isachardot}less{\isacharunderscore}def} may directly be used to unfold the
   definition.  Theorems from the local interpretation disappear after
   leaving the proof context --- that is, after the closing a
   \isakeyword{next} or \isakeyword{qed} statement.%
@@ -121,13 +121,13 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{where}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}lattice\ {\isacharparenleft}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptxt}%
 \normalsize We have already shown that this is a partial
 	order,%
@@ -145,7 +145,7 @@
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \ \ \ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}unfold\ nat{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}%
+\ {\isacharparenleft}unfold\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptxt}%
 \normalsize the goals become \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}inf{\isasymle}x{\isachardot}\ inf\ {\isasymle}\ y\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ z\ {\isasymle}\ x\ {\isasymand}\ z\ {\isasymle}\ y\ {\isasymlongrightarrow}\ z\ {\isasymle}\ inf{\isacharparenright}\isanewline
@@ -165,16 +165,16 @@
 \isamarkuptrue%
 \ \ \ \ \isacommand{then}\isamarkupfalse%
 \ \isacommand{interpret}\isamarkupfalse%
-\ nat{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ int{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
 \isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ min\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ nat{\isachardot}meet{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline
+\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}meet{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline
 \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ {\isasymle}\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ y\ {\isacharequal}\ max\ x\ y{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ nat{\isachardot}join{\isacharunderscore}def\ nat{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
+\ {\isacharparenleft}bestsimp\ simp{\isacharcolon}\ int{\isachardot}join{\isacharunderscore}def\ int{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
 \ \ \isacommand{qed}\isamarkupfalse%
 %
 \endisatagvisible
@@ -186,7 +186,7 @@
 %
 \begin{isamarkuptext}%
 Next follows that \isa{op\ {\isasymle}} is a total order, again for
-  the natural numbers.%
+  the integers.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -196,7 +196,7 @@
 %
 \isatagvisible
 \isacommand{interpretation}\isamarkupfalse%
-\ nat{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ int{\isacharcolon}\ total{\isacharunderscore}order\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isacharcolon}{\isacharcolon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ unfold{\isacharunderscore}locales\ arith%
 \endisatagvisible
@@ -208,26 +208,26 @@
 %
 \begin{isamarkuptext}%
 Theorems that are available in the theory at this point are shown in
-  Table~\ref{tab:nat-lattice}.  Two points are worth noting:
+  Table~\ref{tab:int-lattice}.  Two points are worth noting:
 
 \begin{table}
 \hrule
 \vspace{2ex}
 \begin{center}
 \begin{tabular}{l}
-  \isa{nat{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
+  \isa{int{\isachardot}less{\isacharunderscore}def} from locale \isa{partial{\isacharunderscore}order}: \\
   \quad \isa{{\isacharparenleft}{\isacharquery}x\ {\isacharless}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymle}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}} \\
-  \isa{nat{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
+  \isa{int{\isachardot}meet{\isacharunderscore}left} from locale \isa{lattice}: \\
   \quad \isa{min\ {\isacharquery}x\ {\isacharquery}y\ {\isasymle}\ {\isacharquery}x} \\
-  \isa{nat{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
+  \isa{int{\isachardot}join{\isacharunderscore}distr} from locale \isa{distrib{\isacharunderscore}lattice}: \\
   \quad \isa{max\ {\isacharquery}x\ {\isacharparenleft}min\ {\isacharquery}y\ {\isacharquery}z{\isacharparenright}\ {\isacharequal}\ min\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}y{\isacharparenright}\ {\isacharparenleft}max\ {\isacharquery}x\ {\isacharquery}z{\isacharparenright}} \\
-  \isa{nat{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
+  \isa{int{\isachardot}less{\isacharunderscore}total} from locale \isa{total{\isacharunderscore}order}: \\
   \quad \isa{{\isacharquery}x\ {\isacharless}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}x\ {\isacharequal}\ {\isacharquery}y\ {\isasymor}\ {\isacharquery}y\ {\isacharless}\ {\isacharquery}x}
 \end{tabular}
 \end{center}
 \hrule
-\caption{Interpreted theorems for \isa{{\isasymle}} on the natural numbers.}
-\label{tab:nat-lattice}
+\caption{Interpreted theorems for \isa{{\isasymle}} on the integers.}
+\label{tab:int-lattice}
 \end{table}
 
 \begin{itemize}
@@ -240,7 +240,7 @@
   up in the hierarchy, regardless whether imported or proved via the
   \isakeyword{sublocale} command.
 \item
-  Theorem \isa{nat{\isachardot}less{\isacharunderscore}total} makes use of \isa{op\ {\isacharless}}
+  Theorem \isa{int{\isachardot}less{\isacharunderscore}total} makes use of \isa{op\ {\isacharless}}
   although an equation for the replacement of \isa{op\ {\isasymsqsubset}} was only
   given in the interpretation of \isa{partial{\isacharunderscore}order}.  These
   equations are pushed downwards the hierarchy for related
@@ -461,7 +461,7 @@
   For example, \isakeyword{print\_interps} \isa{partial{\isacharunderscore}order}
   outputs the following:
 \begin{alltt}
-  nat! : partial_order "op \(\le\)"
+  int! : partial_order "op \(\le\)"
   nat_dvd! : partial_order "op dvd"
 \end{alltt}
   The interpretation qualifiers on the left are decorated with an