Reintroduce set_interpreter for Collect and op :.
I removed them by accident when removing old code that dealt with the "set" type.
Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
%
\begin{isabellebody}%
\def\isabellecontext{Tree{\isadigit{2}}}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
\noindent In Exercise~\ref{ex:Tree} we defined a function
\isa{flatten} from trees to lists. The straightforward version of
\isa{flatten} is based on \isa{{\isacharat}} and is thus, like \isa{rev},
quadratic. A linear time version of \isa{flatten} again reqires an extra
argument, the accumulator. Define%
\end{isamarkuptext}%
\isamarkuptrue%
flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent and prove%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: