--- 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)
--- 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