isabelle-cookbook: CookBook/document/root.tex@26e5b41faa74 (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}
89 fee4942c4770 polishing Christian Urban <urbanc@in.tum.de> parents: 85 diff changeset	15	\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	16	\usepackage{pdfsetup}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	18	\urlstyle{rm}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	19	\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	20	\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	21	\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	22	\isadroptag{theory}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	23
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	24	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	25	% 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	26	\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	27	\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	28	\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	29	\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	30	\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	31	\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	32	\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	33	\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	34	\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	35
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	36	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	37	% sane default for proof documents
77 bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	38	\parindent 0pt
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	39	\parskip 0.6ex
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	40	\abovecaptionskip -3mm
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	41	\belowcaptionskip 10mm
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	42	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	43	\hyphenation{Isabelle}
121 26e5b41faa74 polishing Christian Urban <urbanc@in.tum.de> parents: 119 diff changeset	44	\renewcommand{\isasymiota}{}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	45
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	46	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	47	% 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	48	\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	49
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	50	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	51	% 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	52	\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	53	\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	54
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	55	\newcommand{\readmoremarginpar}[1]%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	56	{\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	57
97 a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	58	\newenvironment{leftrightbar}{%
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	59	\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	60	\MakeFramed {\advance\hsize-\width \FrameRestore}}%
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	61	{\endMakeFramed}
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	62
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	63
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	64	\newenvironment{readmore}%
101 123401a5c8e9 tuned Christian Urban <urbanc@in.tum.de> parents: 97 diff changeset	65	{\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	66
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	67	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	68	% 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	69	%(FIXME redefine pagebreak so that it includes a \smallskip)
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	70	\newenvironment{graybox}
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	71	{\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	72	{\smallskip\endMakeFramed}
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	73
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	74	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	75	% 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	76	% 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	77	\newenvironment{vanishML}{%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	78	\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	79	\renewcommand{\isacharverbatimopen}{}%
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	80	\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	81
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	82	\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	83	\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	84	\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	85
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	86	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72 7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	87	% 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	88	\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	89
114 13fd0a83d3c3 properly handled linenumbers in ML-text and Isar-proofs Christian Urban <urbanc@in.tum.de> parents: 108 diff changeset	90	\isakeeptag{linenos}
117 796c6ea633b3 added an option for linenumbers to the chunk-antiquotation Christian Urban <urbanc@in.tum.de> parents: 116 diff changeset	91	\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	92	\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	93
13fd0a83d3c3 properly handled linenumbers in ML-text and Isar-proofs Christian Urban <urbanc@in.tum.de> parents: 108 diff changeset	94	% 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	95	\isakeeptag{linenosgray}
117 796c6ea633b3 added an option for linenumbers to the chunk-antiquotation Christian Urban <urbanc@in.tum.de> parents: 116 diff changeset	96	\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	97	\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	98
115 039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	99	\isakeeptag{small}
039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	100	\renewcommand{\isatagsmall}{\begingroup\small}
039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	101	\renewcommand{\endisatagsmall}{\endgroup}
039845fc96bd some update of the package introduction Christian Urban <urbanc@in.tum.de> parents: 114 diff changeset	102
72 7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	103	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	104	\renewenvironment{isabelle}
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	105	{\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	106	{\end{isabellebody}\end{trivlist}}
85 b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	107
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	108	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	109	% for {* *} in antiquotations
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	110	\newcommand{\isasymverbopen}{\isacharverbatimopen}
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	111	\newcommand{\isasymverbclose}{\isacharverbatimclose}
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	112
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	113	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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	114	% 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	115	\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	116	{\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	117
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	118	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
116 c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	119	% short hands
c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	120	\def\simpleinductive{\isacommand{simple\isacharunderscore{}inductive}}
c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	121
c9ff326e3ce5 more changes to the package chapter Christian Urban <urbanc@in.tum.de> parents: 115 diff changeset	122	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	\begin{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	124
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	125	\title{\mbox{}\\[-10ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	126	\includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
119 4536782969fa added an acknowledgement section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	127	The Isabelle Programming Tutorial (draft)}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	128
119 4536782969fa added an acknowledgement section Christian Urban <urbanc@in.tum.de> parents: 118 diff changeset	129	\author{by Christian Urban with contributions from:\\[2ex]
62 c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	130	\begin{tabular}{r@{\hspace{1.8mm}}l}
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	131	Stefan & Berghofer\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	132	Sascha & Böhme\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	133	Jeremy & Dawson\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	134	Alexander & Krauss\\
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	135	\end{tabular}}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	136
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	137	\maketitle
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	138	\tableofcontents
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	139
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	% generated text of all theories
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	\input{session}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	142
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	143	\newpage
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	144	\bibliographystyle{abbrv}
17 8afa1c990a14 fixed creation of bibliography Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	145	\bibliography{root}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	146
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	147	\end{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	148
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	149	%%% Local Variables:
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	%%% mode: latex
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	%%% TeX-master: t
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Mon, 16 Feb 2009 17:17:24 +0000
changeset 121	26e5b41faa74
parent 119	4536782969fa
child 173	d820cb5873ea
permissions	-rw-r--r--