author  berghofe 
Mon, 22 Jul 2002 13:55:44 +0200  
changeset 13408  024af54a625c 
parent 13406  d587db56ee02 
child 37815  053d23f08946 
permissions  rwrr 
13406  1 
\documentclass[11pt,a4paper]{article} 
2 
\usepackage{isabelle,isabellesym} 

3 
\usepackage{pdfsetup} 

4 

5 
\urlstyle{rm} 

6 
\isabellestyle{it} 

7 

8 
\begin{document} 

9 

10 
\title{Examples for program extraction in HigherOrder Logic} 

11 
\author{Stefan Berghofer} 

12 
\maketitle 

13 

13408
024af54a625c
Added "nocite" to avoid BibTeX error when proofs are switched off.
berghofe
parents:
13406
diff
changeset

14 
\nocite{BergerJAR2001,Coquand93} 
024af54a625c
Added "nocite" to avoid BibTeX error when proofs are switched off.
berghofe
parents:
13406
diff
changeset

15 

13406  16 
\tableofcontents 
17 

18 
\parindent 0pt\parskip 0.5ex 

19 

20 
\input{session} 

21 

22 
\bibliographystyle{abbrv} 

23 
\bibliography{root} 

24 

25 
\end{document} 