# HG changeset patch
# User wenzelm
# Date 926499661 -7200
# Node ID 57abed64dc1408521ebd4d02b2414a67d34f6d6c
# Parent  80052270f08b4a00b3e68819cbc087f2541020da
pdf setup;

diff -r 80052270f08b -r 57abed64dc14 doc-src/Inductive/Makefile
--- a/doc-src/Inductive/Makefile	Wed May 12 09:44:44 1999 +0200
+++ b/doc-src/Inductive/Makefile	Wed May 12 11:01:01 1999 +0200
@@ -1,29 +1,33 @@
-#  $Id$
-#########################################################################
-#									#
-#	Makefile for the report "A Fixedpoint Approach ..."		#
-#									#
-#########################################################################
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
 
-dvi: dist
+
+## dependencies
 
-pdf:
+include ../Makefile.in
 
-FILES =  ind-defs.tex ../proof.sty ../iman.sty ../extra.sty
+NAME = ind-defs
+FILES = ind-defs.tex ../proof.sty ../iman.sty ../extra.sty
 
-ind-defs.dvi.gz:   $(FILES) 
-	-rm ind-defs.dvi.gz
-	latex ind-defs
-	bibtex ind-defs
-	latex ind-defs
-	latex ind-defs
-	gzip -f ind-defs.dvi
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES)
+	$(LATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(LATEX) $(NAME)
 
-dist:   $(FILES) 
-	-rm ind-defs.dvi*
-	latex ind-defs
-	latex ind-defs
+pdf: $(NAME).pdf
 
-clean:
-	@rm *.aux *.log *.toc
-
+$(NAME).pdf: $(FILES)
+	$(PDFLATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(PDFLATEX) $(NAME)
+	$(FIXBOOKMARKS) $(NAME).out
+	$(PDFLATEX) $(NAME)
diff -r 80052270f08b -r 57abed64dc14 doc-src/Inductive/ind-defs.tex
--- a/doc-src/Inductive/ind-defs.tex	Wed May 12 09:44:44 1999 +0200
+++ b/doc-src/Inductive/ind-defs.tex	Wed May 12 11:01:01 1999 +0200
@@ -1,6 +1,6 @@
 %% $Id$
 \documentclass[12pt]{article}
-\usepackage{a4,latexsym,../iman,../extra,../proof}
+\usepackage{a4,latexsym,../iman,../extra,../proof,../pdfsetup}
 
 \newif\ifshort%''Short'' means a published version, not the documentation
 \shortfalse%%%%%\shorttrue
@@ -614,7 +614,7 @@
 \]
 where $+$ denotes addition on the natural numbers and @ denotes append.
 
-\subsection{Rule inversion: the function {\tt mk\_cases}}
+\subsection{Rule inversion: the function \texttt{mk\_cases}}
 The elimination rule, {\tt listn.elim}, is cumbersome:
 \[ \infer{Q}{x\in\listn(A) & 
           \infer*{Q}{[x = \pair{0,\Nil}]} &
@@ -1326,7 +1326,7 @@
 
 
 \begin{footnotesize}
-\bibliographystyle{springer}
+\bibliographystyle{plain}
 \bibliography{../manual}
 \end{footnotesize}
 %%%%%\doendnotes