# HG changeset patch
# User clasohm
# Date 752847907 -3600
# Node ID 329b5ac27f6e518080d0437b4fac67bda33f205c
# Parent  dd350da66c2c389601e6f76558388ce06db255ec
renamed int-prover.ML to intprover.ML,
used exact theory names for use_thy

diff -r dd350da66c2c -r 329b5ac27f6e src/FOLP/Makefile
--- a/src/FOLP/Makefile	Tue Nov 09 13:21:41 1993 +0100
+++ b/src/FOLP/Makefile	Tue Nov 09 13:25:07 1993 +0100
@@ -18,7 +18,7 @@
 
 BIN = $(ISABELLEBIN)
 COMP = $(ISABELLECOMP)
-FILES =  ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML int-prover.ML simpdata.ML\
+FILES =  ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML intprover.ML simpdata.ML\
 	 classical.ML ../Provers/simp.ML ../Provers/ind.ML
 
 $(BIN)/FOLP:   $(BIN)/Pure  $(FILES) 
diff -r dd350da66c2c -r 329b5ac27f6e src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Tue Nov 09 13:21:41 1993 +0100
+++ b/src/FOLP/ROOT.ML	Tue Nov 09 13:25:07 1993 +0100
@@ -16,8 +16,8 @@
 open Readthy;
 
 print_depth 1;  
-use_thy "ifolp";
-use_thy "folp";
+use_thy "IFOLP";
+use_thy "FOLP";
 
 use "../Provers/hypsubst.ML";
 use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
@@ -47,7 +47,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 =