# HG changeset patch # User berghofe # Date 1027259141 -7200 # Node ID d587db56ee027f4b9aead7e358e02cbf681e7f76 # Parent d20a4e67afc8d29f1a599216f7d4112c3d32b8ff Document for program extraction in HOL. diff -r d20a4e67afc8 -r d587db56ee02 src/HOL/Extraction/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/document/root.bib Sun Jul 21 15:45:41 2002 +0200 @@ -0,0 +1,18 @@ +@Article{Berger-JAR-2001, + author = {Ulrich Berger and Helmut Schwichtenberg and Monika Seisenberger}, + title = {The {Warshall} Algorithm and {Dickson's} Lemma: Two + Examples of Realistic Program Extraction}, + journal = {Journal of Automated Reasoning}, + publisher = {Kluwer Academic Publishers}, + year = 2001, + volume = 26, + pages = {205--221} +} + +@TechReport{Coquand93, + author = {Thierry Coquand and Daniel Fridlender}, + title = {A proof of {Higman's} lemma by structural induction}, + institution = {Chalmers University}, + year = 1993, + month = {November} +} diff -r d20a4e67afc8 -r d587db56ee02 src/HOL/Extraction/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Extraction/document/root.tex Sun Jul 21 15:45:41 2002 +0200 @@ -0,0 +1,23 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} +\usepackage{pdfsetup} + +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Examples for program extraction in Higher-Order Logic} +\author{Stefan Berghofer} +\maketitle + +\tableofcontents + +\parindent 0pt\parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document}