1.1 --- a/doc-src/TutorialI/Advanced/advanced.tex Thu Jul 26 17:32:28 2012 +0200
1.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex Thu Jul 26 18:55:42 2012 +0200
1.3 @@ -5,13 +5,13 @@
1.4 yet and which are worth learning. The sections of this chapter are
1.5 independent of each other and can be read in any order.
1.6
1.7 -\input{Advanced/document/simp2.tex}
1.8 +\input{document/simp2.tex}
1.9
1.10 \section{Advanced Induction Techniques}
1.11 \label{sec:advanced-ind}
1.12 \index{induction|(}
1.13 -\input{Misc/document/AdvancedInd.tex}
1.14 -\input{CTL/document/CTLind.tex}
1.15 +\input{document/AdvancedInd.tex}
1.16 +\input{document/CTLind.tex}
1.17 \index{induction|)}
1.18
1.19 %\section{Advanced Forms of Recursion}
1.20 @@ -34,16 +34,16 @@
1.21
1.22 %\subsection{Beyond Measure}
1.23 %\label{sec:beyond-measure}
1.24 -%\input{Advanced/document/WFrec.tex}
1.25 +%\input{document/WFrec.tex}
1.26 %
1.27 %\subsection{Recursion Over Nested Datatypes}
1.28 %\label{sec:nested-recdef}
1.29 -%\input{Recdef/document/Nested0.tex}
1.30 -%\input{Recdef/document/Nested1.tex}
1.31 -%\input{Recdef/document/Nested2.tex}
1.32 +%\input{document/Nested0.tex}
1.33 +%\input{document/Nested1.tex}
1.34 +%\input{document/Nested2.tex}
1.35 %
1.36 %\subsection{Partial Functions}
1.37 %\index{functions!partial}
1.38 -%\input{Advanced/document/Partial.tex}
1.39 +%\input{document/Partial.tex}
1.40 %
1.41 %\index{recdef@\isacommand {recdef} (command)|)}
2.1 --- a/doc-src/TutorialI/CTL/ctl.tex Thu Jul 26 17:32:28 2012 +0200
2.2 +++ b/doc-src/TutorialI/CTL/ctl.tex Thu Jul 26 18:55:42 2012 +0200
2.3 @@ -1,6 +1,6 @@
2.4 \index{model checking example|(}%
2.5 \index{lfp@{\texttt{lfp}}!applications of|see{CTL}}
2.6 -\input{CTL/document/Base.tex}
2.7 -\input{CTL/document/PDL.tex}
2.8 -\input{CTL/document/CTL.tex}
2.9 +\input{document/Base.tex}
2.10 +\input{document/PDL.tex}
2.11 +\input{document/CTL.tex}
2.12 \index{model checking example|)}
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/TutorialI/Documents/documents.tex Thu Jul 26 18:55:42 2012 +0200
3.3 @@ -0,0 +1,24 @@
3.4 +
3.5 +\chapter{Presenting Theories}
3.6 +\label{ch:thy-present}
3.7 +
3.8 +By now the reader should have become sufficiently acquainted with elementary
3.9 +theory development in Isabelle/HOL\@. The following interlude describes
3.10 +how to present theories in a typographically
3.11 +pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
3.12 +of the underlying $\lambda$-calculus language (see
3.13 +{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
3.14 +based on existing PDF-{\LaTeX} technology (see
3.15 +{\S}\ref{sec:document-preparation}).
3.16 +
3.17 +As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
3.18 +years ago, \emph{notions} are in principle more important than
3.19 +\emph{notations}, but suggestive textual representation of ideas is vital to
3.20 +reduce the mental effort to comprehend and apply them.
3.21 +
3.22 +\input{document/Documents.tex}
3.23 +
3.24 +%%% Local Variables:
3.25 +%%% mode: latex
3.26 +%%% TeX-master: t
3.27 +%%% End:
4.1 --- a/doc-src/TutorialI/Inductive/inductive.tex Thu Jul 26 17:32:28 2012 +0200
4.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex Thu Jul 26 18:55:42 2012 +0200
4.3 @@ -18,14 +18,14 @@
4.4 See {\S}\ref{sec:ind-predicates}.
4.5 \end{warn}
4.6
4.7 -\input{Inductive/document/Even}
4.8 -\input{Inductive/document/Mutual}
4.9 -\input{Inductive/document/Star}
4.10 +\input{document/Even}
4.11 +\input{document/Mutual}
4.12 +\input{document/Star}
4.13
4.14 \section{Advanced Inductive Definitions}
4.15 \label{sec:adv-ind-def}
4.16 -\input{Inductive/document/Advanced}
4.17 +\input{document/Advanced}
4.18
4.19 -\input{Inductive/document/AB}
4.20 +\input{document/AB}
4.21
4.22 \index{inductive definitions|)}
5.1 --- a/doc-src/TutorialI/Makefile Thu Jul 26 17:32:28 2012 +0200
5.2 +++ b/doc-src/TutorialI/Makefile Thu Jul 26 18:55:42 2012 +0200
5.3 @@ -13,16 +13,15 @@
5.4 NAME = tutorial
5.5 FILES = tutorial.tex basics.tex fp.tex appendix.tex \
5.6 Advanced/advanced.tex CTL/ctl.tex Inductive/inductive.tex \
5.7 - Inductive/document/AB.tex Inductive/document/Advanced.tex \
5.8 - Inductive/document/Even.tex Inductive/document/Mutual.tex \
5.9 - Inductive/document/Star.tex Protocol/protocol.tex \
5.10 - Protocol/document/Event.tex Protocol/document/Message.tex \
5.11 - Protocol/document/Public.tex Protocol/document/NS_Public.tex \
5.12 - Rules/rules.tex Sets/sets.tex Types/numerics.tex \
5.13 - Types/types.tex Types/document/Overloading.tex \
5.14 - Types/document/Axioms.tex Documents/documents.tex Misc/document/appendix.tex ../iman.sty \
5.15 - ../ttbox.sty ../extra.sty ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty \
5.16 - ../pdfsetup.sty
5.17 + document/AB.tex document/Advanced.tex document/Even.tex \
5.18 + document/Mutual.tex document/Star.tex Protocol/protocol.tex \
5.19 + document/Event.tex document/Message.tex document/Public.tex \
5.20 + document/NS_Public.tex Rules/rules.tex Sets/sets.tex \
5.21 + Types/numerics.tex Types/types.tex document/Overloading.tex \
5.22 + document/Axioms.tex Documents/documents.tex \
5.23 + document/appendix.tex ../iman.sty ../ttbox.sty ../extra.sty \
5.24 + ../../lib/texinputs/isabelle.sty \
5.25 + ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty
5.26
5.27 dvi: $(NAME).dvi
5.28
6.1 --- a/doc-src/TutorialI/Protocol/protocol.tex Thu Jul 26 17:32:28 2012 +0200
6.2 +++ b/doc-src/TutorialI/Protocol/protocol.tex Thu Jul 26 18:55:42 2012 +0200
6.3 @@ -129,7 +129,7 @@
6.4 \index{Needham-Schroeder protocol|)}
6.5
6.6
6.7 -\input{Protocol/document/Message}
6.8 -\input{Protocol/document/Event}
6.9 -\input{Protocol/document/Public}
6.10 -\input{Protocol/document/NS_Public}
6.11 +\input{document/Message}
6.12 +\input{document/Event}
6.13 +\input{document/Public}
6.14 +\input{document/NS_Public}
7.1 --- a/doc-src/TutorialI/Rules/rules.tex Thu Jul 26 17:32:28 2012 +0200
7.2 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Jul 26 18:55:42 2012 +0200
7.3 @@ -1809,7 +1809,7 @@
7.4
7.5 \section{Finding More Theorems}
7.6 \label{sec:find2}
7.7 -\input{Rules/document/find2.tex}
7.8 +\input{document/find2.tex}
7.9
7.10
7.11 \section{Forward Proof: Transforming Theorems}\label{sec:forward}
8.1 --- a/doc-src/TutorialI/Types/types.tex Thu Jul 26 17:32:28 2012 +0200
8.2 +++ b/doc-src/TutorialI/Types/types.tex Thu Jul 26 18:55:42 2012 +0200
8.3 @@ -22,10 +22,10 @@
8.4 is about, but consult the rest only when necessary.
8.5
8.6 \index{pairs and tuples|(}
8.7 -\input{Types/document/Pairs} %%%Section "Pairs and Tuples"
8.8 +\input{document/Pairs} %%%Section "Pairs and Tuples"
8.9 \index{pairs and tuples|)}
8.10
8.11 -\input{Types/document/Records} %%%Section "Records"
8.12 +\input{document/Records} %%%Section "Records"
8.13
8.14
8.15 \section{Type Classes} %%%Section
8.16 @@ -55,15 +55,15 @@
8.17 \label{sec:overloading}
8.18 \index{overloading|(}
8.19
8.20 -\input{Types/document/Overloading}
8.21 +\input{document/Overloading}
8.22
8.23 \index{overloading|)}
8.24
8.25 -\input{Types/document/Axioms}
8.26 +\input{document/Axioms}
8.27
8.28 \index{type classes|)}
8.29 \index{*class|)}
8.30
8.31 \input{Types/numerics} %%%Section "Numbers"
8.32
8.33 -\input{Types/document/Typedefs} %%%Section "Introducing New Types"
8.34 +\input{document/Typedefs} %%%Section "Introducing New Types"
9.1 --- a/doc-src/TutorialI/appendix.tex Thu Jul 26 17:32:28 2012 +0200
9.2 +++ b/doc-src/TutorialI/appendix.tex Thu Jul 26 18:55:42 2012 +0200
9.3 @@ -111,7 +111,7 @@
9.4 \label{tab:ascii}
9.5 \end{table}\indexbold{ASCII@\textsc{ascii} symbols}
9.6
9.7 -\input{Misc/document/appendix.tex}
9.8 +\input{document/appendix.tex}
9.9
9.10 \begin{table}[htbp]
9.11 \begin{center}
10.1 --- a/doc-src/TutorialI/document/Nested.tex Thu Jul 26 17:32:28 2012 +0200
10.2 +++ b/doc-src/TutorialI/document/Nested.tex Thu Jul 26 18:55:42 2012 +0200
10.3 @@ -43,7 +43,7 @@
10.4 would be something like
10.5 \medskip
10.6
10.7 -\input{Datatype/document/unfoldnested.tex}
10.8 +\input{document/unfoldnested.tex}
10.9 \medskip
10.10
10.11 \noindent
11.1 --- a/doc-src/TutorialI/document/documents.tex Thu Jul 26 17:32:28 2012 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,24 +0,0 @@
11.4 -
11.5 -\chapter{Presenting Theories}
11.6 -\label{ch:thy-present}
11.7 -
11.8 -By now the reader should have become sufficiently acquainted with elementary
11.9 -theory development in Isabelle/HOL\@. The following interlude describes
11.10 -how to present theories in a typographically
11.11 -pleasing manner. Isabelle provides a rich infrastructure for concrete syntax
11.12 -of the underlying $\lambda$-calculus language (see
11.13 -{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts
11.14 -based on existing PDF-{\LaTeX} technology (see
11.15 -{\S}\ref{sec:document-preparation}).
11.16 -
11.17 -As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300
11.18 -years ago, \emph{notions} are in principle more important than
11.19 -\emph{notations}, but suggestive textual representation of ideas is vital to
11.20 -reduce the mental effort to comprehend and apply them.
11.21 -
11.22 -\input{Documents/document/Documents.tex}
11.23 -
11.24 -%%% Local Variables:
11.25 -%%% mode: latex
11.26 -%%% TeX-master: t
11.27 -%%% End:
12.1 --- a/doc-src/TutorialI/fp.tex Thu Jul 26 17:32:28 2012 +0200
12.2 +++ b/doc-src/TutorialI/fp.tex Thu Jul 26 18:55:42 2012 +0200
12.3 @@ -32,7 +32,7 @@
12.4 \end{figure}
12.5
12.6 \index{*ToyList example|(}
12.7 -{\makeatother\medskip\input{ToyList/document/ToyList.tex}}
12.8 +{\makeatother\medskip\input{document/ToyList.tex}}
12.9
12.10 The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
12.11 concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
12.12 @@ -203,12 +203,12 @@
12.13 {\S}\ref{sec:fun}.
12.14
12.15 \begin{exercise}\label{ex:Tree}
12.16 -\input{Misc/document/Tree.tex}%
12.17 +\input{document/Tree.tex}%
12.18 \end{exercise}
12.19
12.20 -\input{Misc/document/case_exprs.tex}
12.21 +\input{document/case_exprs.tex}
12.22
12.23 -\input{Ifexpr/document/Ifexpr.tex}
12.24 +\input{document/Ifexpr.tex}
12.25 \index{datatypes|)}
12.26
12.27
12.28 @@ -222,18 +222,18 @@
12.29 \label{sec:nat}\index{natural numbers}%
12.30 \index{linear arithmetic|(}
12.31
12.32 -\input{Misc/document/fakenat.tex}\medskip
12.33 -\input{Misc/document/natsum.tex}
12.34 +\input{document/fakenat.tex}\medskip
12.35 +\input{document/natsum.tex}
12.36
12.37 \index{linear arithmetic|)}
12.38
12.39
12.40 \subsection{Pairs}
12.41 -\input{Misc/document/pairs.tex}
12.42 +\input{document/pairs.tex}
12.43
12.44 \subsection{Datatype {\tt\slshape option}}
12.45 \label{sec:option}
12.46 -\input{Misc/document/Option2.tex}
12.47 +\input{document/Option2.tex}
12.48
12.49 \section{Definitions}
12.50 \label{sec:Definitions}
12.51 @@ -252,9 +252,9 @@
12.52 \commdx{type\protect\_synonym} command:
12.53
12.54 \medskip
12.55 -\input{Misc/document/types.tex}
12.56 +\input{document/types.tex}
12.57
12.58 -\input{Misc/document/prime_def.tex}
12.59 +\input{document/prime_def.tex}
12.60
12.61
12.62 \section{The Definitional Approach}
12.63 @@ -331,19 +331,19 @@
12.64 can be coded and installed, but they are definitely not a matter for this
12.65 tutorial.
12.66
12.67 -\input{Misc/document/simp.tex}
12.68 +\input{document/simp.tex}
12.69
12.70 \index{simplification|)}
12.71
12.72 -\input{Misc/document/Itrev.tex}
12.73 +\input{document/Itrev.tex}
12.74 \begin{exercise}
12.75 -\input{Misc/document/Plus.tex}%
12.76 +\input{document/Plus.tex}%
12.77 \end{exercise}
12.78 \begin{exercise}
12.79 -\input{Misc/document/Tree2.tex}%
12.80 +\input{document/Tree2.tex}%
12.81 \end{exercise}
12.82
12.83 -\input{CodeGen/document/CodeGen.tex}
12.84 +\input{document/CodeGen.tex}
12.85
12.86
12.87 \section{Advanced Datatypes}
12.88 @@ -360,12 +360,12 @@
12.89 \subsection{Mutual Recursion}
12.90 \label{sec:datatype-mut-rec}
12.91
12.92 -\input{Datatype/document/ABexpr.tex}
12.93 +\input{document/ABexpr.tex}
12.94
12.95 \subsection{Nested Recursion}
12.96 \label{sec:nested-datatype}
12.97
12.98 -{\makeatother\input{Datatype/document/Nested.tex}}
12.99 +{\makeatother\input{document/Nested.tex}}
12.100
12.101
12.102 \subsection{The Limits of Nested Recursion}
12.103 @@ -392,7 +392,7 @@
12.104 infinitely branching tree is accepted:
12.105 \smallskip
12.106
12.107 -\input{Datatype/document/Fundata.tex}
12.108 +\input{document/Fundata.tex}
12.109
12.110 If you need nested recursion on the left of a function arrow, there are
12.111 alternatives to pure HOL\@. In the Logic for Computable Functions
12.112 @@ -462,7 +462,7 @@
12.113 information is stored only in the final node associated with the string, many
12.114 nodes do not carry any value. This distinction is modeled with the help
12.115 of the predefined datatype \isa{option} (see {\S}\ref{sec:option}).
12.116 -\input{Trie/document/Trie.tex}
12.117 +\input{document/Trie.tex}
12.118 \index{tries|)}
12.119
12.120 \section{Total Recursive Functions: \isacommand{fun}}
12.121 @@ -479,6 +479,6 @@
12.122 supplied termination proofs, nested recursion and partiality, are discussed
12.123 in a separate tutorial~\cite{isabelle-function}.
12.124
12.125 -\input{Fun/document/fun0.tex}
12.126 +\input{document/fun0.tex}
12.127
12.128 \index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}
13.1 --- a/doc-src/TutorialI/tutorial.tex Thu Jul 26 17:32:28 2012 +0200
13.2 +++ b/doc-src/TutorialI/tutorial.tex Thu Jul 26 18:55:42 2012 +0200
13.3 @@ -64,7 +64,7 @@
13.4 \part{Elementary Techniques}
13.5 \include{basics}
13.6 \include{fp}
13.7 -\include{Documents/documents}
13.8 +\include{documents}
13.9
13.10 \part{Logic and Sets}
13.11 \include{Rules/rules}