isabelle-cookbook: CookBook/document/root.tex@bdd82350cf22 (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}
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	44
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	45	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	46	% 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	47	\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	48
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	49	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	50	% 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	51	\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	52	\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	53
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	54	\newcommand{\readmoremarginpar}[1]%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	55	{\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	56
97 a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	57	\newenvironment{leftrightbar}{%
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	58	\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	59	\MakeFramed {\advance\hsize-\width \FrameRestore}}%
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	60	{\endMakeFramed}
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	61
a99aa67455f3 changed the readmore environment Christian Urban <urbanc@in.tum.de> parents: 89 diff changeset	62
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	63	\newenvironment{readmore}%
101 123401a5c8e9 tuned Christian Urban <urbanc@in.tum.de> parents: 97 diff changeset	64	{\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	65
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	66	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	67	% 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	68	%(FIXME redefine pagebreak so that it includes a \smallskip)
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	69	\newenvironment{graybox}
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	70	{\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	71	{\smallskip\endMakeFramed}
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	72
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	73	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	74	% 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	75	% 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	76	\newenvironment{vanishML}{%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	77	\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	78	\renewcommand{\isacharverbatimopen}{}%
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	79	\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	80
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	81	\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	82	\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	83	\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	84
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	85	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
72 7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	86	% for code that has line numbers
51 c346c156a7cd completes the recipie on antiquotations Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	87	\isakeeptag{linenumbers}
77 bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	88	\renewcommand{\isataglinenumbers}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
bca83ed1d45a changed definition of graybox Christian Urban <urbanc@in.tum.de> parents: 74 diff changeset	89	\renewcommand{\endisataglinenumbers}{\par\end{graybox}\end{vanishML}}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	90
72 7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	91	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	92	\renewenvironment{isabelle}
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays Christian Urban <urbanc@in.tum.de> parents: 71 diff changeset	93	{\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	94	{\end{isabellebody}\end{trivlist}}
85 b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	95
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	96	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	97	% for {* *} in antiquotations
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	98	\newcommand{\isasymverbopen}{\isacharverbatimopen}
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	99	\newcommand{\isasymverbclose}{\isacharverbatimclose}
b02904872d6b better handling of {* and } Christian Urban <urbanc@in.tum.de>* parents: 77 diff changeset	100
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	101	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	\begin{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	103
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	104	\title{\mbox{}\\[-10ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	105	\includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
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	106	The Isabelle Programming Tutorial (fragment)}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	107
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	108	\author{with contributions by:\\[2ex]
62 c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	109	\begin{tabular}{r@{\hspace{1.8mm}}l}
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	110	Stefan & Berghofer\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	111	Sascha & Böhme\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	112	Jeremy & Dawson\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	113	Alexander & Krauss\\
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	114	\end{tabular}}
71 14c3dd5ee2ad removed mytable from root-file Christian Urban <urbanc@in.tum.de> parents: 69 diff changeset	115
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	\maketitle
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	\tableofcontents
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	118
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	119	% generated text of all theories
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	\input{session}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	121
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	122	\newpage
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	123	\bibliographystyle{abbrv}
17 8afa1c990a14 fixed creation of bibliography Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	124	\bibliography{root}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	125
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	126	\end{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	127
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	%%% Local Variables:
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	%%% mode: latex
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	%%% TeX-master: t
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Mon, 09 Feb 2009 01:23:35 +0000
changeset 106	bdd82350cf22
parent 101	123401a5c8e9
child 108	8bea3f74889d
permissions	-rw-r--r--