--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Sun Nov 12 14:48:25 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Sun Nov 12 14:48:47 2000 +0100
@@ -2,8 +2,25 @@
\begin{isabellebody}%
\def\isabellecontext{Advanced}%
\isanewline
-\isacommand{theory}\ Advanced\ {\isacharequal}\ Main{\isacharcolon}\isanewline
+\isacommand{theory}\ Advanced\ {\isacharequal}\ Even{\isacharcolon}%
+\begin{isamarkuptext}%
+We completely forgot about "rule inversion", or whatever we may want
+to call it. Just as a demo I include the two forms that Markus has made available. First the one for binding the result to a name%
+\end{isamarkuptext}%
+\isacommand{inductive{\isacharunderscore}cases}\ even{\isacharunderscore}cases\ {\isacharbrackleft}elim{\isacharbang}{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}\isanewline
\isanewline
+\isacommand{thm}\ even{\isacharunderscore}cases%
+\begin{isamarkuptext}%
+and now the one for local usage:%
+\end{isamarkuptext}%
+\isacommand{lemma}\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}ind{\isacharunderscore}cases\ {\isachardoublequote}Suc{\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isachardoublequote}{\isacharparenright}%
+\begin{isamarkuptext}%
+Both forms accept lists of strings.
+
+Hope you can find some more exciting examples, although these may do%
+\end{isamarkuptext}%
\isacommand{datatype}\ {\isacharprime}f\ {\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Apply\ {\isacharprime}f\ {\isachardoublequote}{\isacharprime}f\ term\ list{\isachardoublequote}\isanewline
\isanewline
\isacommand{consts}\ terms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ term\ set{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Sun Nov 12 14:48:25 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Sun Nov 12 14:48:47 2000 +0100
@@ -29,13 +29,13 @@
Isabelle will not complain because the three definitions do not overlap: no
two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
-benign because the type of \isa{inverse} becomes smaller: on the left it is
+benign because the type of \isa{Overloading{\isadigit{0}}{\isachardot}inverse} becomes smaller: on the left it is
\isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do
-intentionally define \isa{inverse} only at instances of its declared type
+intentionally define \isa{Overloading{\isadigit{0}}{\isachardot}inverse} only at instances of its declared type
\isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
-\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}},
+\isa{Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ Overloading{\isadigit{0}}{\isachardot}inverse\ {\isacharbrackleft}{\isacharbrackright}},
although we never defined inverse on lists. We hasten to say that there is
nothing wrong with such terms and theorems. But it would be nice if we could
prevent their formation, simply because it is very likely that the user did