isabelle-cookbook: ProgTutorial/document/root.tex@0150cf5982ae (annotated)

2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	1	\documentclass[11pt,a4paper]{report}
62 c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	2	\usepackage[latin1]{inputenc}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	\usepackage{amsmath,amsthm}
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	4	\usepackage{isabelle}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	5	\usepackage{isabellesym}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	6	\usepackage{charter}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	7	\usepackage[pdftex]{graphicx}
21 2356e5c70d98 added a proof and tuned the rest Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	8	\usepackage{proof}
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	9	\usepackage{rail}
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	10	\usepackage{url}
38 e21b2f888fa2 added a preliminary section about parsing Christian Urban <urbanc@in.tum.de> parents: 37 diff changeset	11	\usepackage[a4paper,hscale=0.67,vscale=0.76]{geometry}
51 c346c156a7cd completes the recipie on antiquotations Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	12	\usepackage{lineno}
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	13	\usepackage{xcolor}
77 bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	14	\usepackage{framed}
173 d820cb5873ea used latex package boxedminipage Christian Urban <urbanc@in.tum.de> parents: 121 diff changeset	15	\usepackage{boxedminipage}
89 fee4942c4770 polishing Christian Urban <urbanc@in.tum.de> parents: 85 diff changeset	16	\usepackage{mathpartir}
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	17	\usepackage{pdfsetup}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	18
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	19	\urlstyle{rm}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	20	\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	21	\renewcommand{\isastyleminor}{\tt\slshape}%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	22	\renewcommand{\isastyle}{\small\tt\slshape}%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	23	\isadroptag{theory}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	24
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	25	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	26	% For cross references to the other manuals:
7 d7cebb2c5105 added an explicit file containing references in the Implementation manual (should be replaced by antiquotations) Christian Urban <urbanc@in.tum.de> parents: 5 diff changeset	27	\usepackage{xr}
d7cebb2c5105 added an explicit file containing references in the Implementation manual (should be replaced by antiquotations) Christian Urban <urbanc@in.tum.de> parents: 5 diff changeset	28	\externaldocument[I-]{implementation}
d7cebb2c5105 added an explicit file containing references in the Implementation manual (should be replaced by antiquotations) Christian Urban <urbanc@in.tum.de> parents: 5 diff changeset	29	\newcommand{\impref}[1]{\ref{I-#1}}
13 2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	30	\newcommand{\ichcite}[1]{[Impl.\,Man., Ch.~\impref{#1}]}
2b07da8b310d polished and added a subdirectory for the recipes Christian Urban <urbanc@in.tum.de> parents: 7 diff changeset	31	\newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]}
44 dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual Christian Urban <urbanc@in.tum.de> parents: 43 diff changeset	32	\externaldocument[R-]{isar-ref}
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual Christian Urban <urbanc@in.tum.de> parents: 43 diff changeset	33	\newcommand{\isarref}[1]{\ref{R-#1}}
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual Christian Urban <urbanc@in.tum.de> parents: 43 diff changeset	34	\newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]}
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual Christian Urban <urbanc@in.tum.de> parents: 43 diff changeset	35	\newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	36
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	37	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	38	% sane default for proof documents
77 bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	39	\parindent 0pt
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	40	\parskip 0.6ex
173 d820cb5873ea used latex package boxedminipage Christian Urban <urbanc@in.tum.de> parents: 121 diff changeset	41	\abovecaptionskip 1mm
77 bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	42	\belowcaptionskip 10mm
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	43	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	44	\hyphenation{Isabelle}
121 26e5b41faa74 polishing Christian Urban <urbanc@in.tum.de> parents: 119 diff changeset	45	\renewcommand{\isasymiota}{}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	46
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	47	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	48	% to work around a problem with \isanewline
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	49	\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	50
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	51	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	52	% for exercises, comments and readmores
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	53	\newtheorem{exercise}{Exercise}[section]
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	54	\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	55
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	56	\newcommand{\readmoremarginpar}[1]%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	57	{\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}}
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	58
97 a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	59	\newenvironment{leftrightbar}{%
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	60	\def\FrameCommand##1{\vrule width 2pt \hspace{8pt}##1\hspace{8pt}\vrule width 2pt}%
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	61	\MakeFramed {\advance\hsize-\width \FrameRestore}}%
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	62	{\endMakeFramed}
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	63
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	64
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	65	\newenvironment{readmore}%
101 123401a5c8e9 tuned Christian Urban <urbanc@in.tum.de> parents: 97 diff changeset	66	{\begin{leftrightbar}\small\it{\textbf{Read More}}\\}{\end{leftrightbar}}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	67
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	68	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	69	% this is to draw a gray box around code
77 bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	70	%(FIXME redefine pagebreak so that it includes a \smallskip)
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	71	\newenvironment{graybox}
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	72	{\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\smallskip\FrameRestore}}
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	73	{\smallskip\endMakeFramed}
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	74
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	75	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	76	% this hack is for getting rid of the ML {* ... *}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	77	% scaffolding around function definitions
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	78	\newenvironment{vanishML}{%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	79	\renewcommand{\isacommand}[1]{}%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	80	\renewcommand{\isacharverbatimopen}{}%
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	81	\renewcommand{\isacharverbatimclose}{}}{}
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	82
106 bdd82350cf22 renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious) Christian Urban <urbanc@in.tum.de> parents: 101 diff changeset	83	\isakeeptag{TutorialML}
bdd82350cf22 renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious) Christian Urban <urbanc@in.tum.de> parents: 101 diff changeset	84	\renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}}
bdd82350cf22 renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious) Christian Urban <urbanc@in.tum.de> parents: 101 diff changeset	85	\renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}}
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	86
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	87	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72 7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	88	% for code that has line numbers
118 5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 117 diff changeset	89	\newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\par\nolinenumbers}
117 796c6ea633b3 added an option for linenumbers to the chunk-antiquotation Christian Urban <urbanc@in.tum.de> parents: 116 diff changeset	90
114 13fd0a83d3c3 properly handled linenumbers in ML-text and Isar-proofs Christian Urban <urbanc@in.tum.de> parents: 108 diff changeset	91	\isakeeptag{linenos}
117 796c6ea633b3 added an option for linenumbers to the chunk-antiquotation Christian Urban <urbanc@in.tum.de> parents: 116 diff changeset	92	\renewcommand{\isataglinenos}{\begin{linenos}}
118 5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 117 diff changeset	93	\renewcommand{\endisataglinenos}{\end{linenos}}
114 13fd0a83d3c3 properly handled linenumbers in ML-text and Isar-proofs Christian Urban <urbanc@in.tum.de> parents: 108 diff changeset	94
13fd0a83d3c3 properly handled linenumbers in ML-text and Isar-proofs Christian Urban <urbanc@in.tum.de> parents: 108 diff changeset	95	% should only be used in ML code
13fd0a83d3c3 properly handled linenumbers in ML-text and Isar-proofs Christian Urban <urbanc@in.tum.de> parents: 108 diff changeset	96	\isakeeptag{linenosgray}
117 796c6ea633b3 added an option for linenumbers to the chunk-antiquotation Christian Urban <urbanc@in.tum.de> parents: 116 diff changeset	97	\renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}}
118 5f003fdf2653 polished and added more material to the package chapter Christian Urban <urbanc@in.tum.de> parents: 117 diff changeset	98	\renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	99
177 4e2341f6599d polishing Christian Urban <urbanc@in.tum.de> parents: 173 diff changeset	100	\isakeeptag{gray}
4e2341f6599d polishing Christian Urban <urbanc@in.tum.de> parents: 173 diff changeset	101	\renewcommand{\isataggray}{\begin{graybox}}
4e2341f6599d polishing Christian Urban <urbanc@in.tum.de> parents: 173 diff changeset	102	\renewcommand{\endisataggray}{\end{graybox}}
4e2341f6599d polishing Christian Urban <urbanc@in.tum.de> parents: 173 diff changeset	103
115 039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	104	\isakeeptag{small}
039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	105	\renewcommand{\isatagsmall}{\begingroup\small}
039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	106	\renewcommand{\endisatagsmall}{\endgroup}
039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	107
72 7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	108	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	109	\renewenvironment{isabelle}
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	110	{\begin{trivlist}\begin{isabellebody}\small\item\relax}
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	111	{\end{isabellebody}\end{trivlist}}
85 b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	112
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	113	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	114	% for {* *} in antiquotations
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	115	\newcommand{\isasymverbopen}{\isacharverbatimopen}
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	116	\newcommand{\isasymverbclose}{\isacharverbatimclose}
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	117
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	118	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
108 8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular) Christian Urban <urbanc@in.tum.de>* parents: 106 diff changeset	119	% since * cannot be used in text {...}
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular) Christian Urban <urbanc@in.tum.de>* parents: 106 diff changeset	120	\newenvironment{tabularstar}[2]
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular) Christian Urban <urbanc@in.tum.de>* parents: 106 diff changeset	121	{\begin{tabular}{#1}{#2}}{\end{tabular}}
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular) Christian Urban <urbanc@in.tum.de>* parents: 106 diff changeset	122
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular) Christian Urban <urbanc@in.tum.de>* parents: 106 diff changeset	123	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
116 c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	124	% short hands
c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	125	\def\simpleinductive{\isacommand{simple\isacharunderscore{}inductive}}
c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	126
c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	127	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	\begin{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	129
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	130	\title{\mbox{}\\[-10ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	131	\includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
119 4536782969fa added an acknowledgement section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	132	The Isabelle Programming Tutorial (draft)}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	133
119 4536782969fa added an acknowledgement section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	134	\author{by Christian Urban with contributions from:\\[2ex]
62 c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	135	\begin{tabular}{r@{\hspace{1.8mm}}l}
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	136	Stefan & Berghofer\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	137	Sascha & Böhme\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	138	Jeremy & Dawson\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	139	Alexander & Krauss\\
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	140	\end{tabular}}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	141
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	\maketitle
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	143	\tableofcontents
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	144
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	% generated text of all theories
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	\input{session}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	147
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	148	\newpage
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	149	\bibliographystyle{abbrv}
17 8afa1c990a14 fixed creation of bibliography Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	150	\bibliography{root}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	151
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	\end{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	153
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	154	%%% Local Variables:
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	%%% mode: latex
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	156	%%% TeX-master: t
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Thu, 19 Mar 2009 23:21:26 +0100
changeset 191	0150cf5982ae
parent 189	069d525f8f1d
child 210	db8e302f44c8
permissions	-rw-r--r--