1.1 --- a/doc-src/TutorialI/fp.tex	Thu Jul 26 17:32:28 2012 +0200
     1.2 +++ b/doc-src/TutorialI/fp.tex	Thu Jul 26 18:55:42 2012 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  \end{figure}
     1.5  
     1.6  \index{*ToyList example|(}
     1.7 -{\makeatother\medskip\input{ToyList/document/ToyList.tex}}
     1.8 +{\makeatother\medskip\input{document/ToyList.tex}}
     1.9  
    1.10  The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
    1.11  concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
    1.12 @@ -203,12 +203,12 @@
    1.13  {\S}\ref{sec:fun}.
    1.14  
    1.15  \begin{exercise}\label{ex:Tree}
    1.16 -\input{Misc/document/Tree.tex}%
    1.17 +\input{document/Tree.tex}%
    1.18  \end{exercise}
    1.19  
    1.20 -\input{Misc/document/case_exprs.tex}
    1.21 +\input{document/case_exprs.tex}
    1.22  
    1.23 -\input{Ifexpr/document/Ifexpr.tex}
    1.24 +\input{document/Ifexpr.tex}
    1.25  \index{datatypes|)}
    1.26  
    1.27  
    1.28 @@ -222,18 +222,18 @@
    1.29  \label{sec:nat}\index{natural numbers}%
    1.30  \index{linear arithmetic|(}
    1.31  
    1.32 -\input{Misc/document/fakenat.tex}\medskip
    1.33 -\input{Misc/document/natsum.tex}
    1.34 +\input{document/fakenat.tex}\medskip
    1.35 +\input{document/natsum.tex}
    1.36  
    1.37  \index{linear arithmetic|)}
    1.38  
    1.39  
    1.40  \subsection{Pairs}
    1.41 -\input{Misc/document/pairs.tex}
    1.42 +\input{document/pairs.tex}
    1.43  
    1.44  \subsection{Datatype {\tt\slshape option}}
    1.45  \label{sec:option}
    1.46 -\input{Misc/document/Option2.tex}
    1.47 +\input{document/Option2.tex}
    1.48  
    1.49  \section{Definitions}
    1.50  \label{sec:Definitions}
    1.51 @@ -252,9 +252,9 @@
    1.52  \commdx{type\protect\_synonym} command:
    1.53  
    1.54  \medskip
    1.55 -\input{Misc/document/types.tex}
    1.56 +\input{document/types.tex}
    1.57  
    1.58 -\input{Misc/document/prime_def.tex}
    1.59 +\input{document/prime_def.tex}
    1.60  
    1.61  
    1.62  \section{The Definitional Approach}
    1.63 @@ -331,19 +331,19 @@
    1.64  can be coded and installed, but they are definitely not a matter for this
    1.65  tutorial. 
    1.66  
    1.67 -\input{Misc/document/simp.tex}
    1.68 +\input{document/simp.tex}
    1.69  
    1.70  \index{simplification|)}
    1.71  
    1.72 -\input{Misc/document/Itrev.tex}
    1.73 +\input{document/Itrev.tex}
    1.74  \begin{exercise}
    1.75 -\input{Misc/document/Plus.tex}%
    1.76 +\input{document/Plus.tex}%
    1.77  \end{exercise}
    1.78  \begin{exercise}
    1.79 -\input{Misc/document/Tree2.tex}%
    1.80 +\input{document/Tree2.tex}%
    1.81  \end{exercise}
    1.82  
    1.83 -\input{CodeGen/document/CodeGen.tex}
    1.84 +\input{document/CodeGen.tex}
    1.85  
    1.86  
    1.87  \section{Advanced Datatypes}
    1.88 @@ -360,12 +360,12 @@
    1.89  \subsection{Mutual Recursion}
    1.90  \label{sec:datatype-mut-rec}
    1.91  
    1.92 -\input{Datatype/document/ABexpr.tex}
    1.93 +\input{document/ABexpr.tex}
    1.94  
    1.95  \subsection{Nested Recursion}
    1.96  \label{sec:nested-datatype}
    1.97  
    1.98 -{\makeatother\input{Datatype/document/Nested.tex}}
    1.99 +{\makeatother\input{document/Nested.tex}}
   1.100  
   1.101  
   1.102  \subsection{The Limits of Nested Recursion}
   1.103 @@ -392,7 +392,7 @@
   1.104  infinitely branching tree is accepted:
   1.105  \smallskip
   1.106  
   1.107 -\input{Datatype/document/Fundata.tex}
   1.108 +\input{document/Fundata.tex}
   1.109  
   1.110  If you need nested recursion on the left of a function arrow, there are
   1.111  alternatives to pure HOL\@.  In the Logic for Computable Functions 
   1.112 @@ -462,7 +462,7 @@
   1.113  information is stored only in the final node associated with the string, many
   1.114  nodes do not carry any value. This distinction is modeled with the help
   1.115  of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
   1.116 -\input{Trie/document/Trie.tex}
   1.117 +\input{document/Trie.tex}
   1.118  \index{tries|)}
   1.119  
   1.120  \section{Total Recursive Functions: \isacommand{fun}}
   1.121 @@ -479,6 +479,6 @@
   1.122  supplied termination proofs, nested recursion and partiality, are discussed
   1.123  in a separate tutorial~\cite{isabelle-function}.
   1.124  
   1.125 -\input{Fun/document/fun0.tex}
   1.126 +\input{document/fun0.tex}
   1.127  
   1.128  \index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}