--- a/doc-src/TutorialI/Datatype/Nested.thy Wed Apr 19 13:20:16 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy Wed Apr 19 13:40:42 2000 +0200
@@ -25,8 +25,12 @@
nested recursion can be eliminated in favour of mutual recursion by unfolding
the offending datatypes, here \isa{list}. The result for \isa{term}
would be something like
-\begin{ttbox}
-\input{Datatype/tunfoldeddata}\end{ttbox}
+\medskip
+
+\input{Datatype/document/unfoldnested.tex}
+\medskip
+
+\noindent
Although we do not recommend this unfolding to the user, it shows how to
simulate nested recursion by mutual recursion.
Now we return to the initial definition of \isa{term} using
--- a/doc-src/TutorialI/Datatype/ROOT.ML Wed Apr 19 13:20:16 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ROOT.ML Wed Apr 19 13:40:42 2000 +0200
@@ -1,3 +1,4 @@
use_thy "ABexpr";
+use_thy "unfoldnested";
use_thy "Nested";
use_thy "Fundata";
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Wed Apr 19 13:20:16 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Wed Apr 19 13:40:42 2000 +0200
@@ -22,8 +22,12 @@
nested recursion can be eliminated in favour of mutual recursion by unfolding
the offending datatypes, here \isa{list}. The result for \isa{term}
would be something like
-\begin{ttbox}
-\input{Datatype/tunfoldeddata}\end{ttbox}
+\medskip
+
+\input{Datatype/document/unfoldnested.tex}
+\medskip
+
+\noindent
Although we do not recommend this unfolding to the user, it shows how to
simulate nested recursion by mutual recursion.
Now we return to the initial definition of \isa{term} using
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,3 @@
+\begin{isabelle}%
+\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline
+\isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,8 @@
+(*<*)
+theory unfoldnested = Main:;
+(*>*)
+datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list"
+and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list"
+(*<*)
+end
+(*>*)
--- a/doc-src/TutorialI/IsaMakefile Wed Apr 19 13:20:16 2000 +0200
+++ b/doc-src/TutorialI/IsaMakefile Wed Apr 19 13:40:42 2000 +0200
@@ -64,8 +64,8 @@
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
-$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy Datatype/Nested.thy \
- Datatype/Fundata.thy
+$(LOG)/HOL-Datatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \
+ Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy
@$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Datatype
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/ToyList2/ToyList1 Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,15 @@
+theory ToyList = PreList:
+
+datatype 'a list = Nil ("[]")
+ | Cons 'a "'a list" (infixr "#" 65);
+
+consts app :: "'a list => 'a list => 'a list" (infixr "@" 65)
+ rev :: "'a list => 'a list";
+
+primrec
+"[] @ ys = ys"
+"(x # xs) @ ys = x # (xs @ ys)";
+
+primrec
+"rev [] = []"
+"rev (x # xs) = (rev xs) @ (x # [])";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/ToyList2/ToyList2 Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,17 @@
+lemma app_Nil2 [simp]: "xs @ [] = xs";
+apply(induct_tac xs);
+apply(auto).;
+
+lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
+apply(induct_tac xs);
+apply(auto).;
+
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
+apply(induct_tac xs);
+apply(auto).;
+
+theorem rev_rev [simp]: "rev(rev xs) = xs";
+apply(induct_tac xs);
+apply(auto).;
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/isabelle.sty Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,50 @@
+%%
+%% $Id$
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language)
+
+% isabelle environments
+
+\newcommand{\isabelledefaultstyle}{\small\tt\slshape}
+\newcommand{\isabellestyle}{}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+\newenvironment{isabelle}{%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isabelledefaultstyle\isabellestyle}{}
+
+\newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
+
+\newcommand{\isanewline}{\mbox{}\\\mbox{}}
+
+\chardef\isabraceleft=`\{
+\chardef\isabraceright=`\}
+\chardef\isatilde=`\~
+\chardef\isacircum=`\^
+\chardef\isabackslash=`\\
+
+
+% keyword and section markup
+
+\newcommand{\isacommand}[1]{\emph{\bf #1}}
+\newcommand{\isakeyword}[1]{\emph{\bf #1}}
+\newcommand{\isabeginblock}{\isakeyword{\{}}
+\newcommand{\isaendblock}{\isakeyword{\}}}
+
+\newcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
+\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/isabellesym.sty Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,152 @@
+%%
+%% $Id$
+%%
+%% definitions of many Isabelle symbols
+%%
+
+\usepackage{latexsym}
+%\usepackage[latin1]{inputenc}
+
+\newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack
+%\def\textbrokenbar??? etc
+
+\newcommand{\isasymspacespace}{~~}
+\newcommand{\isasymGamma}{$\Gamma$}
+\newcommand{\isasymDelta}{$\Delta$}
+\newcommand{\isasymTheta}{$\Theta$}
+\newcommand{\isasymLambda}{$\Lambda$}
+\newcommand{\isasymPi}{$\Pi$}
+\newcommand{\isasymSigma}{$\Sigma$}
+\newcommand{\isasymPhi}{$\Phi$}
+\newcommand{\isasymPsi}{$\Psi$}
+\newcommand{\isasymOmega}{$\Omega$}
+\newcommand{\isasymalpha}{$\alpha$}
+\newcommand{\isasymbeta}{$\beta$}
+\newcommand{\isasymgamma}{$\gamma$}
+\newcommand{\isasymdelta}{$\delta$}
+\newcommand{\isasymepsilon}{$\varepsilon$}
+\newcommand{\isasymzeta}{$\zeta$}
+\newcommand{\isasymeta}{$\eta$}
+\newcommand{\isasymtheta}{$\vartheta$}
+\newcommand{\isasymkappa}{$\kappa$}
+\newcommand{\isasymlambda}{$\lambda$}
+\newcommand{\isasymmu}{$\mu$}
+\newcommand{\isasymnu}{$\nu$}
+\newcommand{\isasymxi}{$\xi$}
+\newcommand{\isasympi}{$\pi$}
+\newcommand{\isasymrho}{$\rho$}
+\newcommand{\isasymsigma}{$\sigma$}
+\newcommand{\isasymtau}{$\tau$}
+\newcommand{\isasymphi}{$\varphi$}
+\newcommand{\isasymchi}{$\chi$}
+\newcommand{\isasympsi}{$\psi$}
+\newcommand{\isasymomega}{$\omega$}
+\newcommand{\isasymnot}{\emph{$\neg$}}
+\newcommand{\isasymand}{\emph{$\wedge$}}
+\newcommand{\isasymor}{\emph{$\vee$}}
+\newcommand{\isasymforall}{\emph{$\forall\,$}}
+\newcommand{\isasymexists}{\emph{$\exists\,$}}
+\newcommand{\isasymAnd}{\emph{$\bigwedge\,$}}
+\newcommand{\isasymlceil}{\emph{$\lceil$}}
+\newcommand{\isasymrceil}{\emph{$\rceil$}}
+\newcommand{\isasymlfloor}{\emph{$\lfloor$}}
+\newcommand{\isasymrfloor}{\emph{$\rfloor$}}
+\newcommand{\isasymturnstile}{\emph{$\vdash$}}
+\newcommand{\isasymTurnstile}{\emph{$\models$}}
+\newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}}
+\newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}}
+\newcommand{\isasymcdot}{\emph{$\cdot$}}
+\newcommand{\isasymin}{\emph{$\in$}}
+\newcommand{\isasymsubseteq}{\emph{$\subseteq$}}
+\newcommand{\isasyminter}{\emph{$\cap$}}
+\newcommand{\isasymunion}{\emph{$\cup$}}
+\newcommand{\isasymInter}{\emph{$\bigcap\,$}}
+\newcommand{\isasymUnion}{\emph{$\bigcup\,$}}
+\newcommand{\isasymsqinter}{\emph{$\sqcap$}}
+\newcommand{\isasymsqunion}{\emph{$\sqcup$}}
+\newcommand{\isasymSqinter}{\emph{$\bigsqcap\,$}}
+\newcommand{\isasymSqunion}{\emph{$\bigsqcup\,$}}
+\newcommand{\isasymbottom}{\emph{$\bot$}}
+\newcommand{\isasymdoteq}{\emph{$\doteq$}}
+\newcommand{\isasymequiv}{\emph{$\equiv$}}
+\newcommand{\isasymnoteq}{\emph{$\not=$}}
+\newcommand{\isasymsqsubset}{\emph{$\sqsubset$}}
+\newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}}
+\newcommand{\isasymprec}{\emph{$\prec$}}
+\newcommand{\isasympreceq}{\emph{$\preceq$}}
+\newcommand{\isasymsucc}{\emph{$\succ$}}
+\newcommand{\isasymapprox}{\emph{$\approx$}}
+\newcommand{\isasymsim}{\emph{$\sim$}}
+\newcommand{\isasymsimeq}{\emph{$\simeq$}}
+\newcommand{\isasymle}{\emph{$\le$}}
+\newcommand{\isasymColon}{\emph{$\mathrel{::}$}}
+\newcommand{\isasymleftarrow}{\emph{$\leftarrow$}}
+\newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated
+\newcommand{\isasymrightarrow}{\emph{$\rightarrow$}}
+\newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}}
+\newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated
+\newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}}
+\newcommand{\isasymbow}{\emph{$\frown$}}
+\newcommand{\isasymmapsto}{\emph{$\mapsto$}}
+\newcommand{\isasymleadsto}{\emph{$\leadsto$}}
+\newcommand{\isasymup}{\emph{$\uparrow$}}
+\newcommand{\isasymdown}{\emph{$\downarrow$}}
+\newcommand{\isasymnotin}{\emph{$\notin$}}
+\newcommand{\isasymtimes}{\emph{$\times$}}
+\newcommand{\isasymoplus}{\emph{$\oplus$}}
+\newcommand{\isasymominus}{\emph{$\ominus$}}
+\newcommand{\isasymotimes}{\emph{$\otimes$}}
+\newcommand{\isasymoslash}{\emph{$\oslash$}}
+\newcommand{\isasymsubset}{\emph{$\subset$}}
+\newcommand{\isasyminfinity}{\emph{$\infty$}}
+\newcommand{\isasymbox}{\emph{$\Box$}}
+\newcommand{\isasymdiamond}{\emph{$\Diamond$}}
+\newcommand{\isasymcirc}{\emph{$\circ$}}
+\newcommand{\isasymbullet}{\emph{$\bullet$}}
+\newcommand{\isasymparallel}{\emph{$\parallel$}}
+\newcommand{\isasymsurd}{\emph{$\surd$}}
+\newcommand{\isasymcopyright}{\emph{\copyright}}
+
+\newcommand{\isasymplusminus}{\emph{$\pm$}}
+\newcommand{\isasymdiv}{\emph{$\div$}}
+\newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}}
+\newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}}
+\newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}}
+\newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}}
+\newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}}
+\newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}}
+%requires OT1 encoding:
+\newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}}
+\newcommand{\isasymhyphen}{-}
+\newcommand{\isasymmacron}{\={}}
+\newcommand{\isasymexclamdown}{\emph{\textexclamdown}}
+\newcommand{\isasymquestiondown}{\emph{\textquestiondown}}
+%requires OT1 encoding:
+\newcommand{\isasymguillemotleft}{\emph{\guillemotleft}}
+%requires OT1 encoding:
+\newcommand{\isasymguillemotright}{\emph{\guillemotright}}
+%should be available (?):
+\newcommand{\isasymdegree}{\emph{\textdegree}}
+\newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}}
+\newcommand{\isasymonequarter}{\emph{\textonequarter}}
+\newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}}
+\newcommand{\isasymonehalf}{\emph{\textonehalf}}
+\newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}}
+\newcommand{\isasymthreequarters}{\emph{\textthreequarters}}
+\newcommand{\isasymparagraph}{\emph{\P}}
+\newcommand{\isasymregistered}{\emph{\textregistered}}
+%should be available (?):
+\newcommand{\isasymordfeminine}{\emph{\textordfeminine}}
+%should be available (?):
+\newcommand{\isasymordmasculine}{\emph{\textordmasculine}}
+\newcommand{\isasymsection}{\S}
+\newcommand{\isasympounds}{\emph{$\pounds$}}
+%requires OT1 encoding:
+\newcommand{\isasymyen}{\emph{\textyen}}
+%requires OT1 encoding:
+\newcommand{\isasymcent}{\emph{\textcent}}
+%requires OT1 encoding:
+\newcommand{\isasymcurrency}{\emph{\textcurrency}}
+\newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}}
+\newcommand{\isasymrbrace}{\emph{$\mathclose{\mid\mkern-4.5mu\rbrace}$}}
+\newcommand{\isasymtop}{\emph{$\top$}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/pdfsetup.sty Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,9 @@
+%%
+%% $Id$
+%%
+%% conditional url/hyperref setup
+%%
+
+\@ifundefined{pdfoutput}{\usepackage{url}}
+{\usepackage[pdftex,a4paper,colorlinks=true]{hyperref}
+ \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}