isabelle-cookbook: CookBook/document/root.tex@02f76f1b6e7b (annotated)

2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	1	\documentclass[11pt,a4paper]{report}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	\usepackage{amsmath,amsthm}
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	3	\usepackage{isabelle}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	4	\usepackage{isabellesym}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	5	\usepackage{charter}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	6	\usepackage[pdftex]{graphicx}
21 2356e5c70d98 added a proof and tuned the rest Christian Urban <urbanc@in.tum.de> parents: 17 diff changeset	7	\usepackage{proof}
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	8	\usepackage{alltt}
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}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	% Cross references to 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	14	\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	15	\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	16	\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	17	\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	18	\newcommand{\isccite}[1]{[Impl.\,Man., Sec.~\impref{#1}]}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	\usepackage{pdfsetup}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	\urlstyle{rm}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	24	\renewcommand{\isastyleminor}{\tt\slshape}%
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	25	\renewcommand{\isastyle}{\small\tt\slshape}%
41 b11653b11bd3 further progress on the parsing section and tuning on the antiqu's Christian Urban <urbanc@in.tum.de> parents: 39 diff changeset	26	\isadroptag{theory}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	27
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	28	% sane default for proof documents
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	29	\parindent 0pt\parskip 0.6ex
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	30
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	31	% for comments on the margin
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	32	\newcommand{\readmoremarginpar}[1]%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	33	{\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	34
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	35	\newenvironment{readmore}%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	36	{\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	37
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	38	% to work around a problem with \isanewline
42 cd612b489504 tuned mostly antiquotation and text Christian Urban <urbanc@in.tum.de> parents: 41 diff changeset	39	\renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}}
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	40
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	41	\renewenvironment{isabelle}
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	42	{\begin{trivlist}\begin{isabellebody}\small\item\relax}
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	43	{\end{isabellebody}\end{trivlist}}
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	44
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: 13 diff changeset	45	% for exercises and comments
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	\newtheorem{exercise}{Exercise}[section]
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: 13 diff changeset	47	\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	48
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	49	% a table environment with proper indentation
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	50	\newenvironment{mytable}{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}}{\end{tabular}\end{trivlist}}
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	51
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	52	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	53	\hyphenation{Isabelle}
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	54
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	\begin{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	56
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	57	\title{\mbox{}\\[-10ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	58	\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	59	The Isabelle Programmer's Cookbook (fragment)}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	60	\author{with contributions by:\\[2ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	61	\begin{tabular}{l}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	62	Alexander Krauss\\
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	63	Jeremy Dawson\\
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	64	Stefan Berghofer
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	65	\end{tabular}}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	\maketitle
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	67
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	\tableofcontents
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	69
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	70
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	% generated text of all theories
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	\input{session}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	73
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	74	\newpage
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	75	\bibliographystyle{abbrv}
17 8afa1c990a14 fixed creation of bibliography Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	76	\bibliography{root}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	77
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	\end{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	79
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	%%% Local Variables:
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	%%% mode: latex
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	%%% TeX-master: t
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Wed, 29 Oct 2008 13:58:36 +0100
changeset 43	02f76f1b6e7b
parent 42	cd612b489504
child 44	dee4b3e66dfe
permissions	-rw-r--r--