--- a/doc-src/TutorialI/Misc/document/natsum.tex Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Thu Dec 02 14:47:07 2004 +0100
@@ -34,20 +34,20 @@
\newcommand{\mystar}{*%
}
\index{arithmetic operations!for \protect\isa{nat}}%
-The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
-\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
+The arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
+\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
\sdx{div}, \sdx{mod}, \cdx{min} and
\cdx{max} are predefined, as are the relations
-\indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
+\isadxboldpos{\isasymle}{$HOL2arithrel} and
+\isadxboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
\isa{m\ {\isacharless}\ n}. There is even a least number operation
\sdx{LEAST}\@. For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}.
\begin{warn}\index{overloading}
The constants \cdx{0} and \cdx{1} and the operations
- \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
- \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
- \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
- \ttindexboldpos{<}{$HOL2arithrel} are overloaded: they are available
+ \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
+ \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
+ \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
+ \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
not just for natural numbers but for other types as well.
For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
@@ -65,6 +65,12 @@
overloaded operations.
\end{warn}
\begin{warn}
+ The symbols \isadxboldpos{>}{$HOL2arithrel} and
+ \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \isa{x\ {\isachargreater}\ y}
+ stands for \isa{y\ {\isacharless}\ x} and similary for \isa{{\isasymge}} and
+ \isa{{\isasymle}}.
+\end{warn}
+\begin{warn}
Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to equal \isa{Suc\ {\isadigit{0}}}. This definition
(see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
--- a/doc-src/TutorialI/Misc/natsum.thy Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/Misc/natsum.thy Thu Dec 02 14:47:07 2004 +0100
@@ -23,20 +23,20 @@
text{*\newcommand{\mystar}{*%
}
\index{arithmetic operations!for \protect\isa{nat}}%
-The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
-\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
+The arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
+\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
\sdx{div}, \sdx{mod}, \cdx{min} and
\cdx{max} are predefined, as are the relations
-\indexboldpos{\isasymle}{$HOL2arithrel} and
-\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if
+\isadxboldpos{\isasymle}{$HOL2arithrel} and
+\isadxboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if
@{prop"m<n"}. There is even a least number operation
\sdx{LEAST}\@. For example, @{prop"(LEAST n. 0 < n) = Suc 0"}.
\begin{warn}\index{overloading}
The constants \cdx{0} and \cdx{1} and the operations
- \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
- \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
- \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
- \ttindexboldpos{<}{$HOL2arithrel} are overloaded: they are available
+ \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
+ \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
+ \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
+ \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
not just for natural numbers but for other types as well.
For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
that you are talking about natural numbers. Hence Isabelle can only infer
@@ -56,6 +56,12 @@
overloaded operations.
\end{warn}
\begin{warn}
+ The symbols \isadxboldpos{>}{$HOL2arithrel} and
+ \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: @{text"x > y"}
+ stands for @{prop"y < x"} and similary for @{text"\<ge>"} and
+ @{text"\<le>"}.
+\end{warn}
+\begin{warn}
Constant @{text"1::nat"} is defined to equal @{term"Suc 0"}. This definition
(see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
tactics (like @{text auto}, @{text simp} and @{text arith}) but not by
--- a/doc-src/TutorialI/Rules/rules.tex Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex Thu Dec 02 14:47:07 2004 +0100
@@ -634,7 +634,7 @@
as $\exists x.\,P$, they let us proceed with a proof. They can be
filled in later, sometimes in stages and often automatically.
-If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{* trace_unify_fail (flag)},
+If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{*trace_unify_fail (flag)},
which makes Isabelle show the cause of unification failures. For example, suppose we are trying to prove this subgoal by assumption:
\begin{isabelle}
\ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
--- a/doc-src/TutorialI/ToyList/ToyList.thy Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy Thu Dec 02 14:47:07 2004 +0100
@@ -24,8 +24,8 @@
@{term"False"}. Because this notation quickly becomes unwieldy, the
datatype declaration is annotated with an alternative syntax: instead of
@{term[source]Nil} and \isa{Cons x xs} we can write
-@{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
-@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+@{term"[]"}\index{$HOL2list@\isa{[]}|bold} and
+@{term"x # xs"}\index{$HOL2list@\isa{\#}|bold}. In fact, this
alternative syntax is the familiar one. Thus the list \isa{Cons True
(Cons False Nil)} becomes @{term"True # False # []"}. The annotation
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
@@ -56,7 +56,7 @@
restriction, the order of items in a theory file is unconstrained. Function
@{text"app"} is annotated with concrete syntax too. Instead of the
prefix syntax @{text"app xs ys"} the infix
-@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+@{term"xs @ ys"}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
form. Both functions are defined recursively:
*}
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Thu Dec 02 14:47:07 2004 +0100
@@ -29,8 +29,8 @@
\isa{False}. Because this notation quickly becomes unwieldy, the
datatype declaration is annotated with an alternative syntax: instead of
\isa{Nil} and \isa{Cons x xs} we can write
-\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
-\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\isa{[]}|bold} and
+\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this
alternative syntax is the familiar one. Thus the list \isa{Cons True
(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
@@ -61,7 +61,7 @@
restriction, the order of items in a theory file is unconstrained. Function
\isa{app} is annotated with concrete syntax too. Instead of the
prefix syntax \isa{app\ xs\ ys} the infix
-\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
form. Both functions are defined recursively:%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Dec 02 14:47:07 2004 +0100
@@ -300,7 +300,7 @@
FIELDS
\begin{isabelle}%
-a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b%
+a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachargreater}a{\isachardot}\ r\ {\isacharless}\ b%
\end{isabelle}
\rulename{dense}
--- a/doc-src/TutorialI/appendix.tex Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/appendix.tex Thu Dec 02 14:47:07 2004 +0100
@@ -62,7 +62,7 @@
\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
\verb$\<exists>!$\\
\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
-\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} &
+\ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} &
\verb$\<epsilon>$\\
\indexboldpos{\isasymcirc}{$HOL1} &
\ttindexbold{o} &
@@ -71,7 +71,7 @@
\ttindexbold{abs}&
\verb$\<bar> \<bar>$\\
\indexboldpos{\isasymle}{$HOL2arithrel}&
-\ttindexboldpos{<=}{$HOL2arithrel}&
+\isadxboldpos{<=}{$HOL2arithrel}&
\verb$\<le>$\\
\indexboldpos{\isasymtimes}{$Isatype}&
\ttindexboldpos{*}{$HOL2arithfun} &
--- a/doc-src/TutorialI/tutorial.sty Thu Dec 02 12:28:09 2004 +0100
+++ b/doc-src/TutorialI/tutorial.sty Thu Dec 02 14:47:07 2004 +0100
@@ -28,6 +28,7 @@
%%%% for indexing constants, symbols, theorems, ...
\newcommand\cdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (constant)}}
\newcommand\sdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (symbol)}}
+\newcommand\sdxpos[2]{\isa{#1}\index{#2@\protect\isa{#1} (symbol)}}
\newcommand\tdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)}}
\newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}}
@@ -51,6 +52,9 @@
\newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@}
\newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@}
+\newcommand{\isadxpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}}\@}
+\newcommand{\isadxboldpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}|bold}\@}
+
%Commented-out the original versions to see what the index looks like without them.
% In any event, they need to use \isa or \protect\isa rather than \texttt.
%%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}