isabelle-cookbook: CookBook/document/root.tex@dee4b3e66dfe (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}]}
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	19	\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	20	\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	21	\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	22	\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	23
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	\usepackage{pdfsetup}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	25
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	\urlstyle{rm}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	\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	28	\renewcommand{\isastyleminor}{\tt\slshape}%
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	29	\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	30	\isadroptag{theory}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	31
5 e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	32	% sane default for proof documents
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	33	\parindent 0pt\parskip 0.6ex
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	% for comments on the margin
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	36	\newcommand{\readmoremarginpar}[1]%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	37	{\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	38
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	39	\newenvironment{readmore}%
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters Christian Urban <urbanc@in.tum.de> parents: 2 diff changeset	40	{\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	41
39 631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	42	% to work around a problem with \isanewline
42 cd612b489504 tuned mostly antiquotation and text Christian Urban <urbanc@in.tum.de> parents: 41 diff changeset	43	\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	44
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	45	\renewenvironment{isabelle}
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	46	{\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	47	{\end{isabellebody}\end{trivlist}}
631d12c25bde substantial changes to the antiquotations (preliminary version) Christian Urban <urbanc@in.tum.de> parents: 38 diff changeset	48
15 9da9ba2b095b added a solution section and some other minor additions Christian Urban <urbanc@in.tum.de> parents: 13 diff changeset	49	% for exercises and comments
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	\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	51	\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	52
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	53	% a table environment with proper indentation
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	54	\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	55
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	56	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
31 53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	57	\hyphenation{Isabelle}
53460ac408b5 Added alltt, rail, and url. berghofe parents: 21 diff changeset	58
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	\begin{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	60
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	61	\title{\mbox{}\\[-10ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	62	\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	63	The Isabelle Programmer's Cookbook (fragment)}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	64	\author{with contributions by:\\[2ex]
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	65	\begin{tabular}{l}
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	66	Alexander Krauss\\
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	67	Jeremy Dawson\\
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	68	Stefan Berghofer
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	69	\end{tabular}}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	\maketitle
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	71
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	\tableofcontents
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	73
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	74
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	% generated text of all theories
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	\input{session}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	77
2 978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	78	\newpage
978a3c2ed7ce split the document into smaller pieces; Christian Urban <urbanc@in.tum.de> parents: 0 diff changeset	79	\bibliographystyle{abbrv}
17 8afa1c990a14 fixed creation of bibliography Christian Urban <urbanc@in.tum.de> parents: 15 diff changeset	80	\bibliography{root}
0 02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	81
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	\end{document}
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	83
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	%%% Local Variables:
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	%%% mode: latex
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	%%% TeX-master: t
02503850a8cf initial commit of Alexander's files Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	%%% End:

author	Christian Urban <urbanc@in.tum.de>
	Wed, 29 Oct 2008 21:46:33 +0100
changeset 44	dee4b3e66dfe
parent 43	02f76f1b6e7b
child 47	4daf913fdbe1
permissions	-rw-r--r--