EX_FILES includes new oracle examples, and uses the
standard abbreviation convention.

--- a/src/FOL/Makefile	Wed Mar 06 10:14:47 1996 +0100
+++ b/src/FOL/Makefile	Wed Mar 06 10:26:43 1996 +0100
@@ -25,10 +25,9 @@
 	 ../Provers/hypsubst.ML ../Provers/classical.ML \
 	 ../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.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/List.ML ex/List.thy ex/Nat.ML ex/Nat.thy\
-	   ex/Nat2.ML ex/Nat2.thy ex/Prolog.ML ex/Prolog.thy ex/prop.ML\
-	   ex/quant.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 ];\