# HG changeset patch
# User paulson
# Date 826104403 -3600
# Node ID f945e3a96b3595b709a0b4f6320575573e8c02b9
# Parent  ac9b58304d620a094a12dbfa44189a11d0b0e9c1
EX_FILES includes new oracle examples, and uses the
standard abbreviation convention.

diff -r ac9b58304d62 -r f945e3a96b35 src/FOL/Makefile
--- 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 ];\