# HG changeset patch
# User wenzelm
# Date 925921570 -7200
# Node ID dc5bf3f40ad3e025cf53b78e62d939adf6eeda9d
# Parent  c1d7791f03145d0ec08c92d0efcf985ee20ac5a2
improved Makefile;

diff -r c1d7791f0314 -r dc5bf3f40ad3 doc-src/AxClass/Makefile
--- a/doc-src/AxClass/Makefile	Wed May 05 18:24:57 1999 +0200
+++ b/doc-src/AxClass/Makefile	Wed May 05 18:26:10 1999 +0200
@@ -1,23 +1,22 @@
-#  $Id$
-#########################################################################
-#									#
-#	Makefile for the report "Introduction to Isabelle"		#
-#									#
-#########################################################################
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+dist: dvi
 
 
-FILES =  axclass.tex style.tex
+## dependencies
 
-axclass.dvi.gz:   $(FILES)
-	-rm axclass.dvi*
-	latex axclass
-	latex axclass
-	gzip -f axclass.dvi
+include ../Makefile.in
 
-dist:   $(FILES)
-	-rm axclass.dvi*
-	latex axclass
-	latex axclass
+NAME = axclass
+FILES = axclass.tex style.tex
 
-clean:
-	@rm *.aux *.log
+dvi: $(NAME).dvi
+
+$(NAME).dvi: $(FILES)
+	$(LATEX) $(NAME)
+	$(LATEX) $(NAME)
diff -r c1d7791f0314 -r dc5bf3f40ad3 doc-src/Intro/Makefile
--- a/doc-src/Intro/Makefile	Wed May 05 18:24:57 1999 +0200
+++ b/doc-src/Intro/Makefile	Wed May 05 18:26:10 1999 +0200
@@ -1,32 +1,28 @@
-#  $Id$
-#########################################################################
-#									#
-#	Makefile for the report "Introduction to Isabelle"		#
-#									#
-#########################################################################
+#
+# $Id$
+#
+
+## targets
+
+default: dvi
+dist: dvi
 
 
-FILES =  intro.tex foundations.tex getting.tex advanced.tex \
-	 ../proof.sty ../iman.sty ../extra.sty
+## dependencies
+
+include ../Makefile.in
+
+NAME = intro
+FILES = intro.tex foundations.tex getting.tex advanced.tex \
+	../proof.sty ../iman.sty ../extra.sty
 
-intro.dvi.gz:   $(FILES)
-	test -r isabelle.eps || ln -s ../gfx/isabelle.eps .
-	-rm intro.dvi*
-	latex intro
-	bibtex intro
-	latex intro
-	latex intro
-	../sedindex intro
-	latex intro
-	gzip -f intro.dvi
+dvi: $(NAME).dvi
 
-dist:   $(FILES)
-	test -r isabelle.eps || ln -s ../gfx/isabelle.eps .
-	-rm intro.dvi*
-	latex intro
-	latex intro
-	../sedindex intro
-	latex intro
-
-clean:
-	@rm *.aux *.log *.toc *.idx
+$(NAME).dvi: $(FILES) isabelle.eps
+	touch $(NAME).ind
+	$(LATEX) $(NAME)
+	$(BIBTEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(LATEX) $(NAME)
+	$(SEDINDEX) $(NAME)
+	$(LATEX) $(NAME)
diff -r c1d7791f0314 -r dc5bf3f40ad3 doc-src/Intro/intro.bbl
--- a/doc-src/Intro/intro.bbl	Wed May 05 18:24:57 1999 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-\begin{thebibliography}{10}
-
-\bibitem{galton90}
-Antony Galton.
-\newblock {\em Logic for Information Technology}.
-\newblock Wiley, 1990.
-
-\bibitem{mgordon-hol}
-M.~J.~C. Gordon and T.~F. Melham.
-\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
-  Order Logic}.
-\newblock Cambridge University Press, 1993.
-
-\bibitem{mgordon79}
-Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.
-\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.
-\newblock LNCS 78. Springer, 1979.
-
-\bibitem{haskell-tutorial}
-Paul Hudak and Joseph~H. Fasel.
-\newblock A gentle introduction to {Haskell}.
-\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
-
-\bibitem{haskell-report}
-Paul Hudak, Simon~Peyton Jones, and Philip Wadler.
-\newblock Report on the programming language {Haskell}: A non-strict, purely
-  functional language.
-\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
-\newblock Version 1.2.
-
-\bibitem{huet75}
-G.~P. Huet.
-\newblock A unification algorithm for typed $\lambda$-calculus.
-\newblock {\em Theoretical Computer Science}, 1:27--57, 1975.
-
-\bibitem{miller-mixed}
-Dale Miller.
-\newblock Unification under a mixed prefix.
-\newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.
-
-\bibitem{nipkow-prehofer}
-Tobias Nipkow and Christian Prehofer.
-\newblock Type reconstruction for type classes.
-\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
-
-\bibitem{nordstrom90}
-Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
-\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
-\newblock Oxford University Press, 1990.
-
-\bibitem{paulson-natural}
-Lawrence~C. Paulson.
-\newblock Natural deduction as higher-order resolution.
-\newblock {\em Journal of Logic Programming}, 3:237--258, 1986.
-
-\bibitem{paulson87}
-Lawrence~C. Paulson.
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
-\newblock Cambridge University Press, 1987.
-
-\bibitem{paulson-found}
-Lawrence~C. Paulson.
-\newblock The foundation of a generic theorem prover.
-\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989.
-
-\bibitem{paulson700}
-Lawrence~C. Paulson.
-\newblock {Isabelle}: The next 700 theorem provers.
-\newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages
-  361--386. Academic Press, 1990.
-
-\bibitem{paulson-handbook}
-Lawrence~C. Paulson.
-\newblock Designing a theorem prover.
-\newblock In S.~Abramsky, D.~M. Gabbay, and T.~S.~E. Maibaum, editors, {\em
-  Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford
-  University Press, 1992.
-
-\bibitem{paulson-ml2}
-Lawrence~C. Paulson.
-\newblock {\em {ML} for the Working Programmer}.
-\newblock Cambridge University Press, 2nd edition, 1996.
-
-\bibitem{pelletier86}
-F.~J. Pelletier.
-\newblock Seventy-five problems for testing automatic theorem provers.
-\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
-\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
-
-\bibitem{reeves90}
-Steve Reeves and Michael Clarke.
-\newblock {\em Logic for Computer Science}.
-\newblock Addison-Wesley, 1990.
-
-\bibitem{suppes72}
-Patrick Suppes.
-\newblock {\em Axiomatic Set Theory}.
-\newblock Dover, 1972.
-
-\bibitem{wos-bledsoe}
-Larry Wos.
-\newblock Automated reasoning and {Bledsoe's} dream for the field.
-\newblock In Robert~S. Boyer, editor, {\em Automated Reasoning: Essays in Honor
-  of {Woody Bledsoe}}, pages 297--342. Kluwer Academic Publishers, 1991.
-
-\end{thebibliography}
diff -r c1d7791f0314 -r dc5bf3f40ad3 doc-src/Intro/intro.ind
--- a/doc-src/Intro/intro.ind	Wed May 05 18:24:57 1999 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-\begin{theindex}
-
-  \item {\tt !!} symbol, 26
-  \item {\tt\%} symbol, 25
-  \item {\tt ::} symbol, 25
-  \item {\tt ==} symbol, 26
-  \item {\tt ==>} symbol, 26
-  \item {\tt =>} symbol, 25
-  \item {\tt =?=} symbol, 26
-  \item {\tt [} symbol, 25
-  \item {\tt [|} symbol, 26
-  \item {\tt ]} symbol, 25
-  \item {\tt\ttlbrace} symbol, 25
-  \item {\tt\ttrbrace} symbol, 25
-  \item {\tt |]} symbol, 26
-
-  \indexspace
-
-  \item {\tt allI} theorem, 38
-  \item arities
-    \subitem declaring, 4, \bold{48}
-  \item {\tt Asm_simp_tac}, 59
-  \item {\tt assume_tac}, 30, 32, 38
-  \item assumptions
-    \subitem deleting, 20
-    \subitem discharge of, 7
-    \subitem lifting over, 14
-    \subitem of main goal, 41
-    \subitem use of, 16, 28
-  \item axioms
-    \subitem Peano, 54
-
-  \indexspace
-
-  \item {\tt ba}, 31
-  \item {\tt back}, 58, 62
-  \item backtracking
-    \subitem Prolog style, 61
-  \item {\tt bd}, 31
-  \item {\tt be}, 31
-  \item {\tt Blast_tac}, 39, 40
-  \item {\tt br}, 31
-  \item {\tt by}, 31
-
-  \indexspace
-
-  \item {\tt choplev}, 37, 38, 64
-  \item classes, 3
-    \subitem built-in, \bold{25}
-  \item classical reasoner, 39
-  \item {\tt conjunct1} theorem, 28
-  \item constants, 3
-    \subitem clashes with variables, 9
-    \subitem declaring, \bold{47}
-    \subitem overloaded, 53
-    \subitem polymorphic, 3
-  \item {\tt CPure} theory, 46
-
-  \indexspace
-
-  \item definitions, 6, \bold{47}
-    \subitem and derived rules, 43--45
-  \item {\tt DEPTH_FIRST}, 63
-  \item destruct-resolution, 22, 30
-  \item {\tt disjE} theorem, 31
-  \item {\tt dres_inst_tac}, 56
-  \item {\tt dresolve_tac}, 30, 33, 39
-
-  \indexspace
-
-  \item eigenvariables, \see{parameters}{8}
-  \item elim-resolution, \bold{20}, 30
-  \item equality
-    \subitem polymorphic, 3
-  \item {\tt eres_inst_tac}, 56
-  \item {\tt eresolve_tac}, 30, 33, 39
-  \item examples
-    \subitem of deriving rules, 41
-    \subitem of induction, 56, 57
-    \subitem of simplification, 59
-    \subitem of tacticals, 37
-    \subitem of theories, 47, 49--53, 55, 60
-    \subitem propositional, 17, 31, 33
-    \subitem with quantifiers, 18, 34, 36, 38
-  \item {\tt exE} theorem, 38
-
-  \indexspace
-
-  \item {\tt FalseE} theorem, 45
-  \item first-order logic, 1
-  \item flex-flex constraints, 6, 26, \bold{29}
-  \item {\tt flexflex_rule}, 29
-  \item forward proof, 21, 24--30
-  \item {\tt fun} type, 1, 4
-  \item function applications, 1, 8
-
-  \indexspace
-
-  \item {\tt Goal}, 30, 41
-  \item {\tt Goalw}, 44
-
-  \indexspace
-
-  \item {\tt has_fewer_prems}, 63
-  \item higher-order logic, 4
-
-  \indexspace
-
-  \item identifiers, 24
-  \item {\tt impI} theorem, 31, 44
-  \item infixes, 51
-  \item instantiation, 56--59
-  \item Isabelle
-    \subitem object-logics supported, i
-    \subitem overview, i
-    \subitem release history, i
-
-  \indexspace
-
-  \item $\lambda$-abstractions, 1, 8, 25
-  \item $\lambda$-calculus, 1
-  \item LCF, i
-  \item LCF system, 15, 27
-  \item level of a proof, 31
-  \item lifting, \bold{14}
-  \item {\tt logic} class, 3, 6, 25
-
-  \indexspace
-
-  \item major premise, \bold{21}
-  \item {\tt Match} exception, 42
-  \item meta-assumptions
-    \subitem syntax of, 22
-  \item meta-equality, \bold{5}, 26
-  \item meta-implication, \bold{5}, 7, 26
-  \item meta-quantifiers, \bold{5}, 8, 26
-  \item meta-rewriting, 43
-  \item mixfix declarations, 51, 52, 55
-  \item ML, i
-  \item {\tt ML} section, 46
-  \item {\tt mp} theorem, 27, 28
-
-  \indexspace
-
-  \item {\tt Nat} theory, 55
-  \item {\tt nat} type, 3
-  \item {\tt not_def} theorem, 44
-  \item {\tt notE} theorem, 57
-  \item {\tt notI} theorem, \bold{44}, 57
-
-  \indexspace
-
-  \item {\tt o} type, 3, 4
-  \item {\tt ORELSE}, 38
-  \item overloading, \bold{4}, 52
-
-  \indexspace
-
-  \item parameters, \bold{8}, 34
-    \subitem lifting over, 15
-  \item {\tt Prolog} theory, 60
-  \item Prolog interpreter, \bold{60}
-  \item proof state, 16
-  \item proofs
-    \subitem commands for, 30
-  \item {\tt PROP} symbol, 26
-  \item {\textit {prop}} type, 25, 26
-  \item {\tt prop} type, 6
-  \item {\tt prth}, 27
-  \item {\tt prthq}, 27, 29
-  \item {\tt prths}, 27
-  \item {\tt Pure} theory, 46
-
-  \indexspace
-
-  \item {\tt qed}, 31, 43
-  \item quantifiers, 5, 8, 34
-
-  \indexspace
-
-  \item {\tt read_instantiate}, 29
-  \item {\tt refl} theorem, 29
-  \item {\tt REPEAT}, 34, 38, 61, 63
-  \item {\tt res_inst_tac}, 56, 59
-  \item reserved words, 24
-  \item resolution, 10, \bold{12}
-    \subitem in backward proof, 15
-    \subitem with instantiation, 56
-  \item {\tt resolve_tac}, 30, 31, 57
-  \item {\tt result}, 31
-  \item {\tt rewrite_goals_tac}, 44, 45
-  \item {\tt rewrite_rule}, 45
-  \item {\tt RL}, 29
-  \item {\tt RLN}, 29
-  \item {\tt RS}, 27, 29
-  \item {\tt RSN}, 27, 29
-  \item rules
-    \subitem declaring, 47
-    \subitem derived, 13, \bold{22}, 41, 43
-    \subitem destruction, 21
-    \subitem elimination, 21
-    \subitem propositional, 6
-    \subitem quantifier, 8
-
-  \indexspace
-
-  \item search
-    \subitem depth-first, 62
-  \item signatures, \bold{9}
-  \item {\tt Simp_tac}, 59
-  \item simplification, 59
-  \item simplification sets, 59
-  \item sort constraints, 25
-  \item sorts, \bold{5}
-  \item {\tt spec} theorem, 28, 36, 38
-  \item {\tt standard}, 27
-  \item substitution, \bold{8}
-  \item {\tt Suc_inject}, 57
-  \item {\tt Suc_neq_0}, 57
-  \item syntax
-    \subitem of types and terms, 25
-
-  \indexspace
-
-  \item tacticals, \bold{19}, 37
-  \item tactics, \bold{19}
-    \subitem assumption, 30
-    \subitem resolution, 30
-  \item {\tt term} class, 3
-  \item terms
-    \subitem syntax of, 1, \bold{25}
-  \item theorems
-    \subitem basic operations on, \bold{27}
-    \subitem printing of, 27
-  \item theories, \bold{9}
-    \subitem defining, 46--56
-  \item {\tt thm} ML type, 27
-  \item {\tt topthm}, 43
-  \item {\tt Trueprop} constant, 6, 7, 26
-  \item type constraints, 25
-  \item type constructors, 1
-  \item type identifiers, 25
-  \item type synonyms, \bold{50}
-  \item types
-    \subitem declaring, \bold{48}
-    \subitem function, 1
-    \subitem higher, \bold{5}
-    \subitem polymorphic, \bold{3}
-    \subitem simple, \bold{1}
-    \subitem syntax of, 1, \bold{25}
-
-  \indexspace
-
-  \item {\tt undo}, 31
-  \item unification
-    \subitem higher-order, \bold{11}, 57
-    \subitem incompleteness of, 11
-  \item unknowns, 10, 25, 34
-    \subitem function, \bold{11}, 29, 34
-  \item {\tt use_thy}, \bold{46, 47}
-
-  \indexspace
-
-  \item variables
-    \subitem bound, 8
-
-\end{theindex}