doc-src/TutorialI/document/unfoldnested.tex

Clarification: free variables allowed in interpreted locale instances.

%
\begin{isabellebody}%
\def\isabellecontext{unfoldnested}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isacommand{datatype}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteopen}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3D}{\isacharequal}}\ Var\ {\isaliteral{27}{\isacharprime}}v\ {\isaliteral{7C}{\isacharbar}}\ App\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{5F}{\isacharunderscore}}list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{and}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{5F}{\isacharunderscore}}list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}v{\isaliteral{2C}{\isacharcomma}}{\isaliteral{27}{\isacharprime}}f{\isaliteral{29}{\isacharparenright}}term{\isaliteral{5F}{\isacharunderscore}}list{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: