doc-src/Ref/Makefile
author clasohm
Sat, 09 Dec 1995 13:36:11 +0100
changeset 1401 0c439768f45c
parent 1111 ba34f9764816
child 2657 448bb82c4003
permissions -rw-r--r--
removed quotes from consts and syntax sections

#  $Id$
#########################################################################
#									#
#	Makefile for the report "The Isabelle Reference Manual"		#
#									#
#########################################################################


FILES =  ref.tex introduction.tex goals.tex tactic.tex tctical.tex\
         thm.tex theories.tex defining.tex syntax.tex substitution.tex\
         simplifier.tex classical.tex theory-syntax.tex\
	 ../iman.sty ../extra.sty

ref.dvi.gz:   $(FILES) 
	-rm ref.dvi.gz
	latex209 ref
	rail ref
	bibtex ref
	latex209 ref
	latex209 ref
	../sedindex ref
	latex209 ref
	gzip -f ref.dvi