# HG changeset patch
# User clasohm
# Date 752847701 -3600
# Node ID dd350da66c2c389601e6f76558388ce06db255ec
# Parent  91e8875e9c455ff7bbb4c75874b8c447ebfd8c0d
renamed int-prover.ML to intprover.ML,
used exact theory names in ROOT.ML

diff -r 91e8875e9c45 -r dd350da66c2c src/FOL/Makefile
--- a/src/FOL/Makefile	Tue Nov 09 11:02:01 1993 +0100
+++ b/src/FOL/Makefile	Tue Nov 09 13:21:41 1993 +0100
@@ -18,7 +18,7 @@
 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-FILES =  ROOT.ML ifol.thy ifol.ML fol.thy fol.ML int-prover.ML simpdata.ML \
+FILES =  ROOT.ML ifol.thy ifol.ML fol.thy fol.ML intprover.ML simpdata.ML \
 	../Provers/classical.ML ../Provers/simplifier.ML ../Provers/ind.ML
 
 $(BIN)/FOL:   $(BIN)/Pure  $(FILES) 
diff -r 91e8875e9c45 -r dd350da66c2c src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Tue Nov 09 11:02:01 1993 +0100
+++ b/src/FOL/ROOT.ML	Tue Nov 09 13:21:41 1993 +0100
@@ -15,8 +15,8 @@
 open Readthy;
 
 print_depth 1;  
-use_thy "ifol";
-use_thy "fol";
+use_thy "IFOL";
+use_thy "FOL";
 
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
@@ -45,7 +45,7 @@
 structure Hypsubst = HypsubstFun(Hypsubst_Data);
 open Hypsubst;
 
-use "int-prover.ML";
+use "intprover.ML";
 
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data =