isabelle-cookbook: CookBook/document/root.tex@19106a9975c1 (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{alltt}
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	10	\usepackage{rail}
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	11	\usepackage{url}
38 e21b2f888fa2 added a preliminary section about parsing Christian Urban <urbanc@in.tum.de> parents: 37 diff changeset	12	\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	13	\usepackage{lineno}
66 d563f8ff6aa0 tuned Christian Urban <urbanc@in.tum.de> parents: 64 diff changeset	14	\usepackage{boxedminipage}
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	15	\usepackage{xcolor}
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
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	24	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 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
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	38	\parindent 0pt\parskip 0.6ex
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	39
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	40	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	41	% 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	42	\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	43
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	44	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	45	% FIXME: WHAT DOES THIS DO?
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	46	\renewenvironment{isabelle}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	47	{\begin{trivlist}\begin{isabellebody}\small\item\relax}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	48	{\end{isabellebody}\end{trivlist}}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	49
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	50	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
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
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	58	\newenvironment{readmore}%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	59	{\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	60
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	61	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	62	% FIXME: THIS SHOULD NOT BE USED ANYMORE
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	63	% a table environment with proper indentation
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	64	\newenvironment{mytable}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	65	{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	66	{\end{tabular}\end{trivlist}}
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	67
43 02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit Christian Urban <urbanc@in.tum.de> parents: 42 diff changeset	68	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	69	\hyphenation{Isabelle}
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	70
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	71	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	72	% 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	73	% 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	74	\newenvironment{vanishML}{%
4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	75	\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	76	\renewcommand{\isacharverbatimopen}{}%
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	77	\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	78
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	79	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	80	\makeatletter\newenvironment{graybox}{%
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	81	\begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}%
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	82	\colorbox{gray!5}{\usebox{\@tempboxa}}
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	83	}\makeatother
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	84
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	85
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	86	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
64 9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 62 diff changeset	87	\isakeeptag{CookBookML}
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	88	\renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}}
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	89	\renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip}
47 4daf913fdbe1 hakked latex so that it does not display ML {* }; general tuning Christian Urban <urbanc@in.tum.de>* parents: 44 diff changeset	90
51 c346c156a7cd completes the recipie on antiquotations Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	91	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c346c156a7cd completes the recipie on antiquotations Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	92	% for line numbers
c346c156a7cd completes the recipie on antiquotations Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	93	\isakeeptag{linenumbers}
69 19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	94	\renewcommand{\isataglinenumbers}
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	95	{\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers}
19106a9975c1 highligted the background of ML-code Christian Urban <urbanc@in.tum.de> parents: 66 diff changeset	96	\renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip}
51 c346c156a7cd completes the recipie on antiquotations Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	97	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c346c156a7cd completes the recipie on antiquotations Christian Urban <urbanc@in.tum.de> parents: 47 diff changeset	98
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	\begin{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	100
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	101	\title{\mbox{}\\[-10ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	102	\includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	103	The Isabelle Programmer's Cookbook (fragment)}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	104	\author{with contributions by:\\[2ex]
62 c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	105	\begin{tabular}{r@{\hspace{1.8mm}}l}
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	106	Stefan & Berghofer\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	107	Sascha & Böhme\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	108	Jeremy & Dawson\\
c3fe4749ef01 added Sacha as contributor Christian Urban <urbanc@in.tum.de> parents: 51 diff changeset	109	Alexander & Krauss\\
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	110	\end{tabular}}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	\maketitle
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	112
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	113	\tableofcontents
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	114
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	% generated text of all theories
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	\input{session}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	117
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	118	\newpage
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	119	\bibliographystyle{abbrv}
17 8afa1c990a14 fixed creation of bibliography Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	120	\bibliography{root}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	121
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	\end{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	123
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	124	%%% Local Variables:
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	125	%%% mode: latex
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	126	%%% TeX-master: t
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Wed, 14 Jan 2009 17:47:49 +0000
changeset 69	19106a9975c1
parent 66	d563f8ff6aa0
child 71	14c3dd5ee2ad
permissions	-rw-r--r--