# HG changeset patch
# User wenzelm
# Date 866799245 -7200
# Node ID b2ecba22b8be7acce3ab7dd02172846ee3c5e037
# Parent  fa14fb9a572c6a42a1070de9faa20ab0096aa9db
removed old Makefile;

diff -r fa14fb9a572c -r b2ecba22b8be src/CCL/Makefile
--- a/src/CCL/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (CCL)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type
-#	make
-#To make the system and test it on standard examples, type 
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes FOL if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-
-SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
-	    Gfp.thy Gfp.ML Lfp.thy Lfp.ML
-
-CCL_FILES = CCL.thy CCL.ML Term.thy Term.ML Type.thy Type.ML \
-	    coinduction.ML Hered.thy Hered.ML Trancl.thy Trancl.ML\
-	    Wfd.thy Wfd.ML genrec.ML typecheck.ML eval.ML Fix.thy Fix.ML
-
-EX_FILES = ex/ROOT.ML ex/Flag.ML ex/Flag.thy ex/List.ML ex/List.thy\
-	   ex/Nat.ML ex/Nat.thy ex/Stream.ML ex/Stream.thy
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)	$(CCL_FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/CCL;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/CCL;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/CCL;\
-		fi;\
-		discgarb -c $(BIN)/CCL;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/CCL" banner;' \
-		       | $(BIN)/FOL;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
-		       | $(BIN)/FOL;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-$(BIN)/FOL:
-	cd ../FOL;  $(MAKE)
-
-test:	ex/ROOT.ML  $(BIN)/CCL	$(EX_FILES)
-	@case `basename "$(COMP)"` in \
-	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
-		       | $(COMP) $(BIN)/CCL;\
-		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CCL;\
-		fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex";' \
-		       | $(BIN)/CCL;\
-		else echo 'exit_use_dir"ex";' | $(BIN)/CCL;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-.PRECIOUS:  $(BIN)/FOL $(BIN)/CCL 
diff -r fa14fb9a572c -r b2ecba22b8be src/CTT/Makefile
--- a/src/CTT/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (CTT)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type  
-#	make
-#To make the system and test it on standard examples, type  
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES =		ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
-		Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML
-
-EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
-
-$(BIN)/CTT:   $(BIN)/Pure  $(FILES) 
-	@if [ -d $${ISABELLEBIN:?}/Pure ];\
-		then echo Bad value for ISABELLEBIN: \
-			$(BIN) is the Isabelle source directory; \
-			exit 1; \
-	fi
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
-			| $(COMP) $(BIN)/Pure;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/CTT;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/CTT;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/CTT;\
-		fi;\
-		discgarb -c $(BIN)/CTT;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/CTT" banner;' \
-		       | $(BIN)/Pure;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
-		       | $(BIN)/Pure;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-$(BIN)/Pure:
-	cd ../Pure;  $(MAKE)
-
-test:	ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CTT ;;\
-	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/CTT;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-.PRECIOUS:  $(BIN)/Pure	 $(BIN)/CTT 
diff -r fa14fb9a572c -r b2ecba22b8be src/Cube/Makefile
--- a/src/Cube/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (Cube)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type  
-#	make 
-#To make the system and test it on standard examples, type  
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-#WARNING: Poly/ML databases may fail if copied or moved!
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES =		ROOT.ML	 Cube.thy  Cube.ML
-
-$(BIN)/Cube:   $(BIN)/Pure  $(FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
-			| $(COMP) $(BIN)/Pure;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/Cube;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/Cube;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/Cube;\
-		fi;\
-		discgarb -c $(BIN)/Cube;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/Cube" banner;' \
-		       | $(BIN)/Pure;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
-		       | $(BIN)/Pure;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-$(BIN)/Pure:
-	cd ../Pure;  $(MAKE)
-
-test:	ex/ROOT.ML ex/ex.ML $(BIN)/Cube
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/Cube ;;\
-	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/Cube;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-.PRECIOUS:  $(BIN)/Pure	 $(BIN)/Cube 
diff -r fa14fb9a572c -r b2ecba22b8be src/FOL/Makefile
--- a/src/FOL/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (FOL)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type  
-#	make
-#To make the system and test it on standard examples, type  
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
-	thy_data.ML cladata.ML \
-	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
-	../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
-
-EX_NAMES = If List Nat Nat2 Prolog declIffOracle IffOracle
-EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML  ex/int.ML ex/intro.ML\
-	   ex/prop.ML ex/quant.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
-
-$(BIN)/FOL:   $(BIN)/Pure  $(FILES) 
-	@if [ -d $${ISABELLEBIN:?}/Pure ];\
-		then echo Bad value for ISABELLEBIN: \
-			$(BIN) is the Isabelle source directory; \
-			exit 1; \
-	fi
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
-		  | $(COMP) $(BIN)/Pure;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/FOL;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/FOL;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/FOL;\
-		fi;\
-		discgarb -c $(BIN)/FOL;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/FOL" banner;' \
-		       | $(BIN)/Pure;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \
-		       | $(BIN)/Pure;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-$(BIN)/Pure:
-	cd ../Pure;  $(MAKE)
-
-test:	ex/ROOT.ML  $(BIN)/FOL	$(EX_FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
-		       | $(COMP) $(BIN)/FOL;\
-		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\
-		fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex";' \
-		       | $(BIN)/FOL;\
-		else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-.PRECIOUS:   $(BIN)/Pure  $(BIN)/FOL 
diff -r fa14fb9a572c -r b2ecba22b8be src/FOLP/Makefile
--- a/src/FOLP/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-#  $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (FOLP)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type  
-#	make
-#To make the system and test it on standard examples, type  
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES =	 ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML\
-	 hypsubst.ML classical.ML simp.ML 
-
-EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\
-	   ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\
-	   ex/prop.ML ex/quant.ML
-
-$(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
-			| $(COMP) $(BIN)/Pure;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/FOLP;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/FOLP;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/FOLP;\
-		fi;\
-		discgarb -c $(BIN)/FOLP;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/FOLP" banner;' \
-		       | $(BIN)/Pure;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
-		       | $(BIN)/Pure;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-$(BIN)/Pure:
-	cd ../Pure;  $(MAKE)
-
-test:	ex/ROOT.ML  $(BIN)/FOLP	 $(EX_FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
-		       | $(COMP) $(BIN)/FOLP;\
-		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\
-		fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex";' \
-		       | $(BIN)/FOLP;\
-		else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-.PRECIOUS:   $(BIN)/Pure  $(BIN)/FOLP 
diff -r fa14fb9a572c -r b2ecba22b8be src/HOL/Makefile
--- a/src/HOL/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,225 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (HOL)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type  
-#	make
-#To make the system and test it on standard examples, type  
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
-	mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
-	Sexp Univ List RelPow Option
-
-FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
-	ind_syntax.ML cladata.ML simpdata.ML\
-	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML\
-	../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
-	../Provers/simplifier.ML ../Provers/splitter.ML\
-	../Provers/nat_transitive.ML \
-	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
-
-$(BIN)/HOL:   $(BIN)/Pure  $(FILES) 
-	@if [ -d $${ISABELLEBIN:?}/Pure ];\
-		then echo Bad value for ISABELLEBIN: \
-			$(BIN) is the Isabelle source directory; \
-			exit 1; \
-	fi
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
-		  | $(COMP) $(BIN)/Pure;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/HOL;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/HOL;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/HOL;\
-		fi;\
-		discgarb -c $(BIN)/HOL;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/HOL" banner;' \
-		       | $(BIN)/Pure;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
-		       | $(BIN)/Pure;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml; exit 1;;\
-	esac
-
-$(BIN)/Pure:
-	cd ../Pure;  $(MAKE)
-
-#### Testing of HOL
-
-#A macro referring to the object-logic (depends on ML compiler)
-#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
-LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
-	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/HOL" ;;\
-	sml*)	echo "$(ISABELLEBIN)/HOL" ;;\
-	*)	echo "echo; echo Bad value for ISABELLECOMP: \
-			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
-	esac`
-
-
-## Inductive definitions: simple examples
-
-INDUCT_FILES =  Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
-
-INDUCT_FILES = Induct/ROOT.ML \
-	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
-
-Induct:	$(BIN)/HOL $(INDUCT_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Induct";quit();' | $(LOGIC); \
-	else echo 'exit_use_dir"Induct";quit();' | $(LOGIC); \
-	fi
-
-
-##IMP-semantics example
-IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
-IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
-
-IMP:	$(BIN)/HOL  $(IMP_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
-	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
-	fi
-
-##Hoare logic
-Hoare_NAMES = Hoare Arith2 Examples
-Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
-	      $(Hoare_NAMES:%=Hoare/%.ML)
-
-Hoare:	$(BIN)/HOL  $(Hoare_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
-	fi
-
-##The integers in HOL
-INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
-
-INTEG_FILES = Integ/ROOT.ML \
-	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
-
-Integ:	$(BIN)/HOL  $(INTEG_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
-	fi
-
-
-##Authentication & Security Protocols
-Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
-	     Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
-
-AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
-
-Auth:	$(BIN)/HOL  $(AUTH_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
-	fi
-
-
-##Properties of substitutions
-SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
-
-SUBST_FILES = Subst/ROOT.ML \
-	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
-
-Subst:	$(BIN)/HOL  $(SUBST_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
-	fi
-
-##Confluence of Lambda-calculus
-LAMBDA_NAMES = Lambda ParRed Commutation Eta
-
-LAMBDA_FILES = Lambda/ROOT.ML \
-	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
-
-Lambda:	 $(BIN)/HOL $(LAMBDA_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
-	       | $(LOGIC);\
-	else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
-	fi
-
-## Type inference without let
-
-W0_NAMES = I Maybe MiniML Type W
-
-W0_FILES = W0/ROOT.ML \
-	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
-
-W0:	$(BIN)/HOL  $(W0_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"W0";quit();' \
-	       | $(LOGIC);\
-	else echo 'exit_use_dir"W0";quit();' | $(LOGIC); \
-	fi
-
-## Type inference with let
-
-MINIML_NAMES = Generalize Instance Maybe MiniML Type W
-
-MINIML_FILES = MiniML/ROOT.ML \
-	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
-
-MiniML: $(BIN)/HOL  $(MINIML_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
-	       | $(LOGIC);\
-	else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
-	fi
-
-##Lexical analysis
-LEX_FILES = Auto AutoChopper Chopper Prefix
-
-LEX_FILES = Lex/ROOT.ML \
-	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
-
-Lex:	$(BIN)/HOL  $(LEX_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
-	fi
-
-##Miscellaneous examples
-EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
-
-EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
-	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
-
-ex:	$(BIN)/HOL  $(EX_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
-	fi
-
-#Full test.
-test:	$(BIN)/HOL \
-		Induct IMP Hoare Lex Integ Auth Subst Lambda  \
-		W0 MiniML IOA AxClasses Quot ex
-	echo 'Test examples ran successfully' > test
-
-.PRECIOUS:  $(BIN)/Pure $(BIN)/HOL 
diff -r fa14fb9a572c -r b2ecba22b8be src/HOLCF/Makefile
--- a/src/HOLCF/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-# $Id$
-############################################################################
-#									   #
-#		    Makefile for Isabelle (HOLCF)			   #
-#									   #
-############################################################################
-
-#To make the system, cd to this directory and type  
-#	make
-#To make the system and test it on standard examples, type 
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes HOL Isabelle if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-THYS = Porder.thy Porder0.thy Pcpo.thy \
-       Fun1.thy Fun2.thy Fun3.thy \
-       Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
-       Cprod1.thy Cprod2.thy Cprod3.thy \
-       Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
-       Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
-       Up1.thy Up2.thy Up3.thy Fix.thy \
-       One.thy Tr.thy \
-       Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy 
-
-ONLYTHYS = 
-
-FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
-        ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
-        ax_ops/thy_ops.ML    ax_ops/thy_syntax.ML \
-        domain/library.ML  domain/syntax.ML   domain/axioms.ML \
-        domain/theorems.ML domain/extender.ML domain/interface.ML
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/HOLCF:	$(BIN)/HOL  $(FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/HOLCF;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/HOLCF;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/HOLCF;\
-		fi;\
-		discgarb -c $(BIN)/HOLCF;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/HOLCF" banner;' \
-		       | $(BIN)/HOL;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
-		       | $(BIN)/HOL;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-$(BIN)/HOL:
-	cd ../HOL;  $(MAKE)
-
-EX_THYS = ex/Classlib.thy\
-	  ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
-	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
-	  ex/Hoare.thy ex/Loop.thy
-
-EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
-
-test:	ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
-		       | $(COMP) $(BIN)/HOLCF;\
-		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF;\
-		fi;;\
-	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'make_html := true; exit_use_dir"ex";' \
-		       | $(BIN)/HOLCF;\
-		else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-.PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF 
-
diff -r fa14fb9a572c -r b2ecba22b8be src/LCF/Makefile
--- a/src/LCF/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (LCF)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type  
-#	make 
-#To make the system and test it on standard examples, type  
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes FOL if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES =	 ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/LCF;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/LCF;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/LCF;\
-		fi;\
-		discgarb -c $(BIN)/LCF;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/LCF" banner;' \
-		       | $(BIN)/FOL;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
-		       | $(BIN)/FOL;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-(BIN)/FOL:
-	cd ../FOL;  $(MAKE)
-
-test:	ex/ROOT.ML ex/ex.ML  $(BIN)/LCF
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/LCF ;;\
-	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/LCF;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-.PRECIOUS:   $(BIN)/FOL	 $(BIN)/LCF 
diff -r fa14fb9a572c -r b2ecba22b8be src/Sequents/Makefile
--- a/src/Sequents/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (Sequents)		#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type
-#	make
-#To make the system and test it on standard examples, type 
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes Pure if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-NAMES = ILL LK S4 S43 T
-FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
-
-ILL_NAMES = ILL_predlog washing 
-EX_FILES = ex/ROOT.ML \
-    ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \
-    ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \
-    ex/ILL/ILL_kleene_lemmas.ML \
-    $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
-
-$(BIN)/Sequents:   $(BIN)/Pure	$(FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'	\
-			| $(COMP) $(BIN)/Pure;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/Sequents;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/Sequents;\
-		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/Sequents;\
-		fi;\
-		discgarb -c $(BIN)/Sequents;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/Sequents" banner;' | $(BIN)/Pure;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/Sequents" banner;' \
-		       | $(BIN)/Pure;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/Sequents" banner;' \
-		       | $(BIN)/Pure;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-$(BIN)/Pure:
-	cd ../Pure;  $(MAKE)
-
-test:	$(BIN)/Sequents	 $(EX_FILES)
-	@case `basename "$(COMP)"` in \
-	poly*)	echo 'exit_use_dir"ex";quit();' | $(COMP) $(BIN)/Sequents;;\
-	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/Sequents;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml;;\
-	esac
-
-
-.PRECIOUS:  $(BIN)/Pure $(BIN)/Sequents 
diff -r fa14fb9a572c -r b2ecba22b8be src/ZF/Makefile
--- a/src/ZF/Makefile	Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-# $Id$
-#########################################################################
-#									#
-#			Makefile for Isabelle (ZF)			#
-#									#
-#########################################################################
-
-#To make the system, cd to this directory and type
-#	make
-#To make the system and test it on standard examples, type 
-#	make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes FOL if this file is ABSENT -- but not 
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-NAMES = ZF upair subset pair domrange \
-	func AC equalities Bool \
-	Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
-	constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
-	WF Order Ordinal Epsilon Arith Univ \
-	QUniv Datatype OrderArith OrderType \
-	Cardinal CardinalArith Cardinal_AC InfDatatype \
-	Zorn Nat Finite List 
-
-FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML\
-	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/ZF:   $(BIN)/FOL	 $(FILES) 
-	@case `basename "$(COMP)"` in \
-	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
-		if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/ZF;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/ZF;\
-		else echo 'open PolyML; exit_use_dir".";' \
-		       | $(COMP) $(BIN)/ZF;\
-		fi;\
-		discgarb -c $(BIN)/ZF;;\
-	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
-		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
-		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
-		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/ZF" banner;' \
-		       | $(BIN)/FOL;\
-		else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
-		       | $(BIN)/FOL;\
-		fi;;\
-	*)	echo Bad value for ISABELLECOMP: \
-			\"$(COMP)\" is not poly or sml; exit 1;;\
-	esac
-
-$(BIN)/FOL:
-	cd ../FOL;  $(MAKE)
-
-#### Testing of ZF
-
-#A macro referring to the object-logic (depends on ML compiler)
-#	[Thanks to Thomas Santen and Stephan Herrmann from GMD First]
-LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
-	poly*)	echo "$(ISABELLECOMP) $(ISABELLEBIN)/ZF" ;;\
-	sml*)	echo "$(ISABELLEBIN)/ZF" ;;\
-	*)	echo "echo; echo Bad value for ISABELLECOMP: \
-			$(ISABELLECOMP) is not poly or sml; exit 1" ;;\
-	esac`
-
-##IMP-semantics example
-IMP_NAMES = Com Denotation Equiv
-IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
-
-IMP:   $(BIN)/ZF  $(IMP_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
-	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
-	fi
-
-##Coinduction example
-COIND_NAMES = ECR MT Map Static Types Values 
-
-COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy\
-	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
-
-Coind:	$(BIN)/ZF  $(COIND_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Coind";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"Coind";quit();' | $(LOGIC); \
-	fi
-
-##AC examples
-AC_NAMES = AC_Equiv Cardinal_aux \
-	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
-	   DC DC_lemmas HH Hartog WO1_AC \
-	   WO2_AC16 WO6_WO1 WO_AC recfunAC16 rel_is_fun
-
-AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
-	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
-	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
-	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
-
-AC:  $(BIN)/ZF	$(AC_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"AC";quit();' | $(LOGIC); \
-	else echo 'exit_use_dir"AC";quit();' | $(LOGIC); \
-	fi
-
-##Residuals example
-
-RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
-	      Cube Residuals Terms
-
-RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) \
-			    $(RESID_NAMES:%=Resid/%.ML)
-
-Resid:	$(BIN)/ZF  $(RESID_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"Resid";quit();' | $(LOGIC);\
-	else echo 'exit_use_dir"Resid";quit();' | $(LOGIC); \
-	fi
-
-##Miscellaneous examples
-EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
-	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit 
-
-EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
-
-#Test ZF by loading the examples in directory ex
-ex:	$(BIN)/ZF  $(EX_FILES)
-	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC); \
-	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
-	fi
-
-#Full test.
-test:	$(BIN)/ZF IMP Coind AC Resid ex
-	echo 'Test examples ran successfully' > test
-
-.PRECIOUS:  $(BIN)/FOL $(BIN)/ZF