*** empty log message ***
authornipkow
Thu Dec 02 14:47:07 2004 +0100 (2004-12-02)
changeset 153640c3891c3528f
parent 15363 885a40edcdba
child 15365 611c32b7f6e5
*** empty log message ***
doc-src/TutorialI/Misc/document/natsum.tex
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/tutorial.sty
     1.1 --- a/doc-src/TutorialI/Misc/document/natsum.tex	Thu Dec 02 12:28:09 2004 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/document/natsum.tex	Thu Dec 02 14:47:07 2004 +0100
     1.3 @@ -34,20 +34,20 @@
     1.4  \newcommand{\mystar}{*%
     1.5  }
     1.6  \index{arithmetic operations!for \protect\isa{nat}}%
     1.7 -The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
     1.8 -\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
     1.9 +The arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
    1.10 +\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
    1.11  \sdx{div}, \sdx{mod}, \cdx{min} and
    1.12  \cdx{max} are predefined, as are the relations
    1.13 -\indexboldpos{\isasymle}{$HOL2arithrel} and
    1.14 -\ttindexboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
    1.15 +\isadxboldpos{\isasymle}{$HOL2arithrel} and
    1.16 +\isadxboldpos{<}{$HOL2arithrel}. As usual, \isa{m\ {\isacharminus}\ n\ {\isacharequal}\ {\isadigit{0}}} if
    1.17  \isa{m\ {\isacharless}\ n}. There is even a least number operation
    1.18  \sdx{LEAST}\@.  For example, \isa{{\isacharparenleft}LEAST\ n{\isachardot}\ {\isadigit{0}}\ {\isacharless}\ n{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}}.
    1.19  \begin{warn}\index{overloading}
    1.20    The constants \cdx{0} and \cdx{1} and the operations
    1.21 -  \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
    1.22 -  \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
    1.23 -  \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
    1.24 -  \ttindexboldpos{<}{$HOL2arithrel} are overloaded: they are available
    1.25 +  \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
    1.26 +  \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
    1.27 +  \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
    1.28 +  \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
    1.29    not just for natural numbers but for other types as well.
    1.30    For example, given the goal \isa{x\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ x}, there is nothing to indicate
    1.31    that you are talking about natural numbers. Hence Isabelle can only infer
    1.32 @@ -65,6 +65,12 @@
    1.33    overloaded operations.
    1.34  \end{warn}
    1.35  \begin{warn}
    1.36 +  The symbols \isadxboldpos{>}{$HOL2arithrel} and
    1.37 +  \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: \isa{x\ {\isachargreater}\ y}
    1.38 +  stands for \isa{y\ {\isacharless}\ x} and similary for \isa{{\isasymge}} and
    1.39 +  \isa{{\isasymle}}.
    1.40 +\end{warn}
    1.41 +\begin{warn}
    1.42    Constant \isa{{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat} is defined to equal \isa{Suc\ {\isadigit{0}}}. This definition
    1.43    (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
    1.44    tactics (like \isa{auto}, \isa{simp} and \isa{arith}) but not by
     2.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Thu Dec 02 12:28:09 2004 +0100
     2.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Thu Dec 02 14:47:07 2004 +0100
     2.3 @@ -23,20 +23,20 @@
     2.4  text{*\newcommand{\mystar}{*%
     2.5  }
     2.6  \index{arithmetic operations!for \protect\isa{nat}}%
     2.7 -The arithmetic operations \ttindexboldpos{+}{$HOL2arithfun},
     2.8 -\ttindexboldpos{-}{$HOL2arithfun}, \ttindexboldpos{\mystar}{$HOL2arithfun},
     2.9 +The arithmetic operations \isadxboldpos{+}{$HOL2arithfun},
    2.10 +\isadxboldpos{-}{$HOL2arithfun}, \isadxboldpos{\mystar}{$HOL2arithfun},
    2.11  \sdx{div}, \sdx{mod}, \cdx{min} and
    2.12  \cdx{max} are predefined, as are the relations
    2.13 -\indexboldpos{\isasymle}{$HOL2arithrel} and
    2.14 -\ttindexboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if
    2.15 +\isadxboldpos{\isasymle}{$HOL2arithrel} and
    2.16 +\isadxboldpos{<}{$HOL2arithrel}. As usual, @{prop"m-n = (0::nat)"} if
    2.17  @{prop"m<n"}. There is even a least number operation
    2.18  \sdx{LEAST}\@.  For example, @{prop"(LEAST n. 0 < n) = Suc 0"}.
    2.19  \begin{warn}\index{overloading}
    2.20    The constants \cdx{0} and \cdx{1} and the operations
    2.21 -  \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun},
    2.22 -  \ttindexboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
    2.23 -  \cdx{max}, \indexboldpos{\isasymle}{$HOL2arithrel} and
    2.24 -  \ttindexboldpos{<}{$HOL2arithrel} are overloaded: they are available
    2.25 +  \isadxboldpos{+}{$HOL2arithfun}, \isadxboldpos{-}{$HOL2arithfun},
    2.26 +  \isadxboldpos{\mystar}{$HOL2arithfun}, \cdx{min},
    2.27 +  \cdx{max}, \isadxboldpos{\isasymle}{$HOL2arithrel} and
    2.28 +  \isadxboldpos{<}{$HOL2arithrel} are overloaded: they are available
    2.29    not just for natural numbers but for other types as well.
    2.30    For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate
    2.31    that you are talking about natural numbers. Hence Isabelle can only infer
    2.32 @@ -56,6 +56,12 @@
    2.33    overloaded operations.
    2.34  \end{warn}
    2.35  \begin{warn}
    2.36 +  The symbols \isadxboldpos{>}{$HOL2arithrel} and
    2.37 +  \isadxboldpos{\isasymge}{$HOL2arithrel} are merely syntax: @{text"x > y"}
    2.38 +  stands for @{prop"y < x"} and similary for @{text"\<ge>"} and
    2.39 +  @{text"\<le>"}.
    2.40 +\end{warn}
    2.41 +\begin{warn}
    2.42    Constant @{text"1::nat"} is defined to equal @{term"Suc 0"}. This definition
    2.43    (see \S\ref{sec:ConstDefinitions}) is unfolded automatically by some
    2.44    tactics (like @{text auto}, @{text simp} and @{text arith}) but not by
     3.1 --- a/doc-src/TutorialI/Rules/rules.tex	Thu Dec 02 12:28:09 2004 +0100
     3.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Thu Dec 02 14:47:07 2004 +0100
     3.3 @@ -634,7 +634,7 @@
     3.4  as $\exists x.\,P$, they let us proceed with a proof.  They can be 
     3.5  filled in later, sometimes in stages and often automatically. 
     3.6  
     3.7 -If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{* trace_unify_fail (flag)},
     3.8 +If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{*trace_unify_fail (flag)},
     3.9  which makes Isabelle show the cause of unification failures.  For example, suppose we are trying to prove this subgoal by assumption:
    3.10  \begin{isabelle}
    3.11  \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
     4.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Thu Dec 02 12:28:09 2004 +0100
     4.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Thu Dec 02 14:47:07 2004 +0100
     4.3 @@ -24,8 +24,8 @@
     4.4  @{term"False"}. Because this notation quickly becomes unwieldy, the
     4.5  datatype declaration is annotated with an alternative syntax: instead of
     4.6  @{term[source]Nil} and \isa{Cons x xs} we can write
     4.7 -@{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
     4.8 -@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
     4.9 +@{term"[]"}\index{$HOL2list@\isa{[]}|bold} and
    4.10 +@{term"x # xs"}\index{$HOL2list@\isa{\#}|bold}. In fact, this
    4.11  alternative syntax is the familiar one.  Thus the list \isa{Cons True
    4.12  (Cons False Nil)} becomes @{term"True # False # []"}. The annotation
    4.13  \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
    4.14 @@ -56,7 +56,7 @@
    4.15  restriction, the order of items in a theory file is unconstrained. Function
    4.16  @{text"app"} is annotated with concrete syntax too. Instead of the
    4.17  prefix syntax @{text"app xs ys"} the infix
    4.18 -@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
    4.19 +@{term"xs @ ys"}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
    4.20  form. Both functions are defined recursively:
    4.21  *}
    4.22  
     5.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Dec 02 12:28:09 2004 +0100
     5.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Thu Dec 02 14:47:07 2004 +0100
     5.3 @@ -29,8 +29,8 @@
     5.4  \isa{False}. Because this notation quickly becomes unwieldy, the
     5.5  datatype declaration is annotated with an alternative syntax: instead of
     5.6  \isa{Nil} and \isa{Cons x xs} we can write
     5.7 -\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\texttt{[]}|bold} and
     5.8 -\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
     5.9 +\isa{{\isacharbrackleft}{\isacharbrackright}}\index{$HOL2list@\isa{[]}|bold} and
    5.10 +\isa{x\ {\isacharhash}\ xs}\index{$HOL2list@\isa{\#}|bold}. In fact, this
    5.11  alternative syntax is the familiar one.  Thus the list \isa{Cons True
    5.12  (Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
    5.13  \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} 
    5.14 @@ -61,7 +61,7 @@
    5.15  restriction, the order of items in a theory file is unconstrained. Function
    5.16  \isa{app} is annotated with concrete syntax too. Instead of the
    5.17  prefix syntax \isa{app\ xs\ ys} the infix
    5.18 -\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
    5.19 +\isa{xs\ {\isacharat}\ ys}\index{$HOL2list@\isa{\at}|bold} becomes the preferred
    5.20  form. Both functions are defined recursively:%
    5.21  \end{isamarkuptext}%
    5.22  \isamarkuptrue%
     6.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Thu Dec 02 12:28:09 2004 +0100
     6.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Thu Dec 02 14:47:07 2004 +0100
     6.3 @@ -300,7 +300,7 @@
     6.4  FIELDS
     6.5  
     6.6  \begin{isabelle}%
     6.7 -a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b%
     6.8 +a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachargreater}a{\isachardot}\ r\ {\isacharless}\ b%
     6.9  \end{isabelle}
    6.10  \rulename{dense}
    6.11  
     7.1 --- a/doc-src/TutorialI/appendix.tex	Thu Dec 02 12:28:09 2004 +0100
     7.2 +++ b/doc-src/TutorialI/appendix.tex	Thu Dec 02 14:47:07 2004 +0100
     7.3 @@ -62,7 +62,7 @@
     7.4  \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
     7.5  \verb$\<exists>!$\\
     7.6  \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
     7.7 -\ttindexbold{SOME}, \texttt{\at}\index{$HOL2list@\texttt{\at}} &
     7.8 +\ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} &
     7.9  \verb$\<epsilon>$\\
    7.10  \indexboldpos{\isasymcirc}{$HOL1} &
    7.11  \ttindexbold{o} &
    7.12 @@ -71,7 +71,7 @@
    7.13  \ttindexbold{abs}&
    7.14  \verb$\<bar> \<bar>$\\
    7.15  \indexboldpos{\isasymle}{$HOL2arithrel}&
    7.16 -\ttindexboldpos{<=}{$HOL2arithrel}&
    7.17 +\isadxboldpos{<=}{$HOL2arithrel}&
    7.18  \verb$\<le>$\\
    7.19  \indexboldpos{\isasymtimes}{$Isatype}&
    7.20  \ttindexboldpos{*}{$HOL2arithfun} &
     8.1 --- a/doc-src/TutorialI/tutorial.sty	Thu Dec 02 12:28:09 2004 +0100
     8.2 +++ b/doc-src/TutorialI/tutorial.sty	Thu Dec 02 14:47:07 2004 +0100
     8.3 @@ -28,6 +28,7 @@
     8.4  %%%% for indexing constants, symbols, theorems, ...
     8.5  \newcommand\cdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (constant)}}
     8.6  \newcommand\sdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (symbol)}}
     8.7 +\newcommand\sdxpos[2]{\isa{#1}\index{#2@\protect\isa{#1} (symbol)}}
     8.8  
     8.9  \newcommand\tdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)}}
    8.10  \newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}}
    8.11 @@ -51,6 +52,9 @@
    8.12  \newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@}
    8.13  \newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@}
    8.14  
    8.15 +\newcommand{\isadxpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}}\@}
    8.16 +\newcommand{\isadxboldpos}[2]{\isa{#1}\index{#2@\protect\isa{#1}|bold}\@}
    8.17 +
    8.18  %Commented-out the original versions to see what the index looks like without them.
    8.19  %   In any event, they need to use \isa or \protect\isa rather than \texttt.
    8.20  %%\newcommand{\indexboldpos}[2]{#1\index{#2@#1|bold}\@}