# HG changeset patch # User wenzelm # Date 1343321742 -7200 # Node ID 708278fc2dff9077d22041861113551b41db7dcb # Parent 0e4bb86c74fd44abbf26ccd9d78f56aadccbc14b recovered latex job; diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/Advanced/advanced.tex --- a/doc-src/TutorialI/Advanced/advanced.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/Advanced/advanced.tex Thu Jul 26 18:55:42 2012 +0200 @@ -5,13 +5,13 @@ yet and which are worth learning. The sections of this chapter are independent of each other and can be read in any order. -\input{Advanced/document/simp2.tex} +\input{document/simp2.tex} \section{Advanced Induction Techniques} \label{sec:advanced-ind} \index{induction|(} -\input{Misc/document/AdvancedInd.tex} -\input{CTL/document/CTLind.tex} +\input{document/AdvancedInd.tex} +\input{document/CTLind.tex} \index{induction|)} %\section{Advanced Forms of Recursion} @@ -34,16 +34,16 @@ %\subsection{Beyond Measure} %\label{sec:beyond-measure} -%\input{Advanced/document/WFrec.tex} +%\input{document/WFrec.tex} % %\subsection{Recursion Over Nested Datatypes} %\label{sec:nested-recdef} -%\input{Recdef/document/Nested0.tex} -%\input{Recdef/document/Nested1.tex} -%\input{Recdef/document/Nested2.tex} +%\input{document/Nested0.tex} +%\input{document/Nested1.tex} +%\input{document/Nested2.tex} % %\subsection{Partial Functions} %\index{functions!partial} -%\input{Advanced/document/Partial.tex} +%\input{document/Partial.tex} % %\index{recdef@\isacommand {recdef} (command)|)} diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/CTL/ctl.tex --- a/doc-src/TutorialI/CTL/ctl.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/CTL/ctl.tex Thu Jul 26 18:55:42 2012 +0200 @@ -1,6 +1,6 @@ \index{model checking example|(}% \index{lfp@{\texttt{lfp}}!applications of|see{CTL}} -\input{CTL/document/Base.tex} -\input{CTL/document/PDL.tex} -\input{CTL/document/CTL.tex} +\input{document/Base.tex} +\input{document/PDL.tex} +\input{document/CTL.tex} \index{model checking example|)} diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/Documents/documents.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Documents/documents.tex Thu Jul 26 18:55:42 2012 +0200 @@ -0,0 +1,24 @@ + +\chapter{Presenting Theories} +\label{ch:thy-present} + +By now the reader should have become sufficiently acquainted with elementary +theory development in Isabelle/HOL\@. The following interlude describes +how to present theories in a typographically +pleasing manner. Isabelle provides a rich infrastructure for concrete syntax +of the underlying $\lambda$-calculus language (see +{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts +based on existing PDF-{\LaTeX} technology (see +{\S}\ref{sec:document-preparation}). + +As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 +years ago, \emph{notions} are in principle more important than +\emph{notations}, but suggestive textual representation of ideas is vital to +reduce the mental effort to comprehend and apply them. + +\input{document/Documents.tex} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/Inductive/inductive.tex --- a/doc-src/TutorialI/Inductive/inductive.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/Inductive/inductive.tex Thu Jul 26 18:55:42 2012 +0200 @@ -18,14 +18,14 @@ See {\S}\ref{sec:ind-predicates}. \end{warn} -\input{Inductive/document/Even} -\input{Inductive/document/Mutual} -\input{Inductive/document/Star} +\input{document/Even} +\input{document/Mutual} +\input{document/Star} \section{Advanced Inductive Definitions} \label{sec:adv-ind-def} -\input{Inductive/document/Advanced} +\input{document/Advanced} -\input{Inductive/document/AB} +\input{document/AB} \index{inductive definitions|)} diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/Makefile --- a/doc-src/TutorialI/Makefile Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/Makefile Thu Jul 26 18:55:42 2012 +0200 @@ -13,16 +13,15 @@ NAME = tutorial FILES = tutorial.tex basics.tex fp.tex appendix.tex \ Advanced/advanced.tex CTL/ctl.tex Inductive/inductive.tex \ - Inductive/document/AB.tex Inductive/document/Advanced.tex \ - Inductive/document/Even.tex Inductive/document/Mutual.tex \ - Inductive/document/Star.tex Protocol/protocol.tex \ - Protocol/document/Event.tex Protocol/document/Message.tex \ - Protocol/document/Public.tex Protocol/document/NS_Public.tex \ - Rules/rules.tex Sets/sets.tex Types/numerics.tex \ - Types/types.tex Types/document/Overloading.tex \ - Types/document/Axioms.tex Documents/documents.tex Misc/document/appendix.tex ../iman.sty \ - ../ttbox.sty ../extra.sty ../../lib/texinputs/isabelle.sty ../../lib/texinputs/isabellesym.sty \ - ../pdfsetup.sty + document/AB.tex document/Advanced.tex document/Even.tex \ + document/Mutual.tex document/Star.tex Protocol/protocol.tex \ + document/Event.tex document/Message.tex document/Public.tex \ + document/NS_Public.tex Rules/rules.tex Sets/sets.tex \ + Types/numerics.tex Types/types.tex document/Overloading.tex \ + document/Axioms.tex Documents/documents.tex \ + document/appendix.tex ../iman.sty ../ttbox.sty ../extra.sty \ + ../../lib/texinputs/isabelle.sty \ + ../../lib/texinputs/isabellesym.sty ../pdfsetup.sty dvi: $(NAME).dvi diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/Protocol/protocol.tex --- a/doc-src/TutorialI/Protocol/protocol.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/Protocol/protocol.tex Thu Jul 26 18:55:42 2012 +0200 @@ -129,7 +129,7 @@ \index{Needham-Schroeder protocol|)} -\input{Protocol/document/Message} -\input{Protocol/document/Event} -\input{Protocol/document/Public} -\input{Protocol/document/NS_Public} +\input{document/Message} +\input{document/Event} +\input{document/Public} +\input{document/NS_Public} diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Jul 26 18:55:42 2012 +0200 @@ -1809,7 +1809,7 @@ \section{Finding More Theorems} \label{sec:find2} -\input{Rules/document/find2.tex} +\input{document/find2.tex} \section{Forward Proof: Transforming Theorems}\label{sec:forward} diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/Types/types.tex --- a/doc-src/TutorialI/Types/types.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/Types/types.tex Thu Jul 26 18:55:42 2012 +0200 @@ -22,10 +22,10 @@ is about, but consult the rest only when necessary. \index{pairs and tuples|(} -\input{Types/document/Pairs} %%%Section "Pairs and Tuples" +\input{document/Pairs} %%%Section "Pairs and Tuples" \index{pairs and tuples|)} -\input{Types/document/Records} %%%Section "Records" +\input{document/Records} %%%Section "Records" \section{Type Classes} %%%Section @@ -55,15 +55,15 @@ \label{sec:overloading} \index{overloading|(} -\input{Types/document/Overloading} +\input{document/Overloading} \index{overloading|)} -\input{Types/document/Axioms} +\input{document/Axioms} \index{type classes|)} \index{*class|)} \input{Types/numerics} %%%Section "Numbers" -\input{Types/document/Typedefs} %%%Section "Introducing New Types" +\input{document/Typedefs} %%%Section "Introducing New Types" diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/appendix.tex --- a/doc-src/TutorialI/appendix.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/appendix.tex Thu Jul 26 18:55:42 2012 +0200 @@ -111,7 +111,7 @@ \label{tab:ascii} \end{table}\indexbold{ASCII@\textsc{ascii} symbols} -\input{Misc/document/appendix.tex} +\input{document/appendix.tex} \begin{table}[htbp] \begin{center} diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/document/Nested.tex --- a/doc-src/TutorialI/document/Nested.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/document/Nested.tex Thu Jul 26 18:55:42 2012 +0200 @@ -43,7 +43,7 @@ would be something like \medskip -\input{Datatype/document/unfoldnested.tex} +\input{document/unfoldnested.tex} \medskip \noindent diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/document/documents.tex --- a/doc-src/TutorialI/document/documents.tex Thu Jul 26 17:32:28 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ - -\chapter{Presenting Theories} -\label{ch:thy-present} - -By now the reader should have become sufficiently acquainted with elementary -theory development in Isabelle/HOL\@. The following interlude describes -how to present theories in a typographically -pleasing manner. Isabelle provides a rich infrastructure for concrete syntax -of the underlying $\lambda$-calculus language (see -{\S}\ref{sec:concrete-syntax}), as well as document preparation of theory texts -based on existing PDF-{\LaTeX} technology (see -{\S}\ref{sec:document-preparation}). - -As pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 -years ago, \emph{notions} are in principle more important than -\emph{notations}, but suggestive textual representation of ideas is vital to -reduce the mental effort to comprehend and apply them. - -\input{Documents/document/Documents.tex} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/fp.tex Thu Jul 26 18:55:42 2012 +0200 @@ -32,7 +32,7 @@ \end{figure} \index{*ToyList example|(} -{\makeatother\medskip\input{ToyList/document/ToyList.tex}} +{\makeatother\medskip\input{document/ToyList.tex}} The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} @@ -203,12 +203,12 @@ {\S}\ref{sec:fun}. \begin{exercise}\label{ex:Tree} -\input{Misc/document/Tree.tex}% +\input{document/Tree.tex}% \end{exercise} -\input{Misc/document/case_exprs.tex} +\input{document/case_exprs.tex} -\input{Ifexpr/document/Ifexpr.tex} +\input{document/Ifexpr.tex} \index{datatypes|)} @@ -222,18 +222,18 @@ \label{sec:nat}\index{natural numbers}% \index{linear arithmetic|(} -\input{Misc/document/fakenat.tex}\medskip -\input{Misc/document/natsum.tex} +\input{document/fakenat.tex}\medskip +\input{document/natsum.tex} \index{linear arithmetic|)} \subsection{Pairs} -\input{Misc/document/pairs.tex} +\input{document/pairs.tex} \subsection{Datatype {\tt\slshape option}} \label{sec:option} -\input{Misc/document/Option2.tex} +\input{document/Option2.tex} \section{Definitions} \label{sec:Definitions} @@ -252,9 +252,9 @@ \commdx{type\protect\_synonym} command: \medskip -\input{Misc/document/types.tex} +\input{document/types.tex} -\input{Misc/document/prime_def.tex} +\input{document/prime_def.tex} \section{The Definitional Approach} @@ -331,19 +331,19 @@ can be coded and installed, but they are definitely not a matter for this tutorial. -\input{Misc/document/simp.tex} +\input{document/simp.tex} \index{simplification|)} -\input{Misc/document/Itrev.tex} +\input{document/Itrev.tex} \begin{exercise} -\input{Misc/document/Plus.tex}% +\input{document/Plus.tex}% \end{exercise} \begin{exercise} -\input{Misc/document/Tree2.tex}% +\input{document/Tree2.tex}% \end{exercise} -\input{CodeGen/document/CodeGen.tex} +\input{document/CodeGen.tex} \section{Advanced Datatypes} @@ -360,12 +360,12 @@ \subsection{Mutual Recursion} \label{sec:datatype-mut-rec} -\input{Datatype/document/ABexpr.tex} +\input{document/ABexpr.tex} \subsection{Nested Recursion} \label{sec:nested-datatype} -{\makeatother\input{Datatype/document/Nested.tex}} +{\makeatother\input{document/Nested.tex}} \subsection{The Limits of Nested Recursion} @@ -392,7 +392,7 @@ infinitely branching tree is accepted: \smallskip -\input{Datatype/document/Fundata.tex} +\input{document/Fundata.tex} If you need nested recursion on the left of a function arrow, there are alternatives to pure HOL\@. In the Logic for Computable Functions @@ -462,7 +462,7 @@ information is stored only in the final node associated with the string, many nodes do not carry any value. This distinction is modeled with the help of the predefined datatype \isa{option} (see {\S}\ref{sec:option}). -\input{Trie/document/Trie.tex} +\input{document/Trie.tex} \index{tries|)} \section{Total Recursive Functions: \isacommand{fun}} @@ -479,6 +479,6 @@ supplied termination proofs, nested recursion and partiality, are discussed in a separate tutorial~\cite{isabelle-function}. -\input{Fun/document/fun0.tex} +\input{document/fun0.tex} \index{fun@\isacommand {fun} (command)|)}\index{functions!total|)} diff -r 0e4bb86c74fd -r 708278fc2dff doc-src/TutorialI/tutorial.tex --- a/doc-src/TutorialI/tutorial.tex Thu Jul 26 17:32:28 2012 +0200 +++ b/doc-src/TutorialI/tutorial.tex Thu Jul 26 18:55:42 2012 +0200 @@ -64,7 +64,7 @@ \part{Elementary Techniques} \include{basics} \include{fp} -\include{Documents/documents} +\include{documents} \part{Logic and Sets} \include{Rules/rules}