--- a/src/CCL/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/CCL/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (CCL) #
+# Makefile for Isabelle (CCL) #
# #
#########################################################################
@@ -26,54 +26,54 @@
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
+ 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)
+$(BIN)/CCL: $(BIN)/FOL $(SET_FILES) $(CCL_FILES)
case "$(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;\
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/FOL:
cd ../FOL; $(MAKE)
-test: ex/ROOT.ML $(BIN)/CCL $(EX_FILES)
+test: ex/ROOT.ML $(BIN)/CCL $(EX_FILES)
case "$(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;;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/FOL $(BIN)/CCL
--- a/src/CTT/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/CTT/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (CTT) #
+# Makefile for Isabelle (CTT) #
# #
#########################################################################
@@ -21,50 +21,50 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
+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;\
+ then echo Bad value for ISABELLEBIN: \
+ $(BIN) is the Isabelle source directory; \
+ exit 1; \
+ fi;\
case "$(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;\
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES)
+test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml;;\
esac
-.PRECIOUS: $(BIN)/Pure $(BIN)/CTT
+.PRECIOUS: $(BIN)/Pure $(BIN)/CTT
--- a/src/Cube/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/Cube/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (Cube) #
+# Makefile for Isabelle (Cube) #
# #
#########################################################################
@@ -22,42 +22,42 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML Cube.thy Cube.ML
+FILES = ROOT.ML Cube.thy Cube.ML
$(BIN)/Cube: $(BIN)/Pure $(FILES)
case "$(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;\
+ 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".";' \
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex.ML $(BIN)/Cube
+test: ex.ML $(BIN)/Cube
case "$(COMP)" in \
poly*) echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/Cube ;;\
sml*) echo 'exit_use"ex.ML";' | $(BIN)/Cube;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml;;\
esac
-.PRECIOUS: $(BIN)/Pure $(BIN)/Cube
+.PRECIOUS: $(BIN)/Pure $(BIN)/Cube
--- a/src/FOL/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/FOL/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (FOL) #
+# Makefile for Isabelle (FOL) #
# #
#########################################################################
@@ -21,7 +21,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
+FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
../Provers/hypsubst.ML ../Provers/classical.ML \
../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
@@ -31,51 +31,51 @@
$(BIN)/FOL: $(BIN)/Pure $(FILES)
if [ -d $${ISABELLEBIN:?}/Pure ];\
- then echo Bad value for ISABELLEBIN: \
- $(BIN) is the Isabelle source directory; \
- exit 1; \
- fi;\
+ then echo Bad value for ISABELLEBIN: \
+ $(BIN) is the Isabelle source directory; \
+ exit 1; \
+ fi;\
case "$(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;\
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES)
+test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES)
case "$(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;;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/FOL
--- a/src/FOLP/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/FOLP/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (FOLP) #
+# Makefile for Isabelle (FOLP) #
# #
#########################################################################
@@ -21,7 +21,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML\
+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\
@@ -32,44 +32,44 @@
case "$(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;\
+ 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".";' \
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES)
+test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES)
case "$(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;;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
.PRECIOUS: $(BIN)/Pure $(BIN)/FOLP
--- a/src/HOL/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/HOL/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (HOL) #
+# Makefile for Isabelle (HOL) #
# #
#########################################################################
@@ -22,44 +22,44 @@
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
+ 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/simplifier.ML ../Provers/splitter.ML\
- $(NAMES:%=%.thy) $(NAMES:%=%.ML)
+ ../Provers/simplifier.ML ../Provers/splitter.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;\
+ then echo Bad value for ISABELLEBIN: \
+ $(BIN) is the Isabelle source directory; \
+ exit 1; \
+ fi;\
case "$(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;\
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml; exit 1;;\
esac
$(BIN)/Pure:
@@ -72,45 +72,45 @@
poly*) echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
sml*) echo "$ISABELLEBIN/HOL" ;;\
*) echo "echo Bad value for ISABELLECOMP: \
- $ISABELLEBIN is not poly or sml; exit 1" ;;\
+ $ISABELLEBIN is not poly or sml; exit 1" ;;\
esac
##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)
+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
+ 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_NAMES:%=Hoare/%.ML)
-Hoare: $(BIN)/HOL $(Hoare_FILES)
+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
+ 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
INTEG_FILES = Integ/ROOT.ML \
- $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
+ $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
-Integ: $(BIN)/HOL $(INTEG_FILES)
+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
+ then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
+ else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
+ fi
##I/O Automata
IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
- Receiver Sender
+ Receiver Sender
IOA_ABP_NAMES = Action Correctness Lemmas
IOA_MT_NAMES = Asig IOA Solve
@@ -122,15 +122,15 @@
$(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML)\
$(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
-IOA: $(BIN)/HOL $(IOA_FILES)
+IOA: $(BIN)/HOL $(IOA_FILES)
if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
- | $(LOGIC);\
- echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
- | $(LOGIC);\
- else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
+ then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
+ | $(LOGIC);\
+ echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
+ | $(LOGIC);\
+ else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
- fi
+ fi
##Authentication & Security Protocols
@@ -138,78 +138,78 @@
AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
-Auth: $(BIN)/HOL $(AUTH_FILES)
+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
+ 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_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
-Subst: $(BIN)/HOL $(SUBST_FILES)
+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
+ 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_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
-Lambda: $(BIN)/HOL $(LAMBDA_FILES)
+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
+ then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
+ | $(LOGIC);\
+ else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
+ fi
##Type inference for MiniML
MINIML_NAMES = I Maybe MiniML Type W
MINIML_FILES = MiniML/ROOT.ML \
- $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.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
+ 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_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
+ 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 Perm Comb InSort Qsort LexProd Puzzle Mutil \
- Primes NatSum SList LList Acc PropLog Term Simult MT
+ Primes NatSum SList LList Acc PropLog Term Simult 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/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
-ex: $(BIN)/HOL $(EX_FILES)
+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
+ 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 IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
+test: $(BIN)/HOL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
echo 'Test examples ran successfully' > test
.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
--- a/src/HOLCF/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/HOLCF/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,8 +1,8 @@
# $Id$
############################################################################
-# #
-# Makefile for Isabelle (HOLCF) #
-# #
+# #
+# Makefile for Isabelle (HOLCF) #
+# #
############################################################################
#To make the system, cd to this directory and type
@@ -33,52 +33,52 @@
FILES = ROOT.ML Porder0.thy $(THYS) $(THYS:.thy=.ML)
#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
+$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
case "$(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;\
+ 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".";' \
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/HOL:
cd ../HOL; $(MAKE)
EX_THYS = ex/Fix2.thy ex/Hoare.thy \
- ex/Loop.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)
+test: ex/ROOT.ML $(BIN)/HOLCF $(EX_FILES)
case "$(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;;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
@@ -89,21 +89,21 @@
EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
$(EXPLICIT_DOMAINS_THYS:.thy=.ML)
-test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES)
+test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES)
case "$(COMP)" in \
poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'make_html := true; exit_use_dir"explicit_domains"; quit();' | $(COMP) $(BIN)/HOLCF;\
- else echo 'exit_use_dir"explicit_domains"; quit();' \
- | $(COMP) $(BIN)/HOLCF;\
- fi;;\
+ then echo 'make_html := true; exit_use_dir"explicit_domains"; quit();' | $(COMP) $(BIN)/HOLCF;\
+ else echo 'exit_use_dir"explicit_domains"; quit();' \
+ | $(COMP) $(BIN)/HOLCF;\
+ fi;;\
sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
- | $(BIN)/HOLCF;\
- else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
- fi;;\
+ then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
+ | $(BIN)/HOLCF;\
+ else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
+ fi;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml;;\
esac
-.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF
+.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF
--- a/src/LCF/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/LCF/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (LCF) #
+# Makefile for Isabelle (LCF) #
# #
#########################################################################
@@ -21,42 +21,42 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
+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 "$(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;\
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
(BIN)/FOL:
cd ../FOL; $(MAKE)
-test: ex.ML $(BIN)/LCF
+test: ex.ML $(BIN)/LCF
case "$(COMP)" in \
poly*) echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\
sml*) echo 'exit_use"ex.ML";' | $(BIN)/LCF;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml;;\
esac
-.PRECIOUS: $(BIN)/FOL $(BIN)/LCF
+.PRECIOUS: $(BIN)/FOL $(BIN)/LCF
--- a/src/Pure/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/Pure/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (Pure) #
+# Makefile for Isabelle (Pure) #
# #
#########################################################################
@@ -24,10 +24,10 @@
FILES = POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\
net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\
- goals.ML axclass.ML install_pp.ML\
- NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
+ goals.ML axclass.ML install_pp.ML\
+ NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
-SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\
+SYNTAX_FILES = Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML\
Syntax/parser.ML Syntax/type_ext.ML Syntax/syn_trans.ML\
Syntax/pretty.ML Syntax/printer.ML Syntax/syntax.ML\
Syntax/syn_ext.ML Syntax/mixfix.ML
@@ -36,25 +36,24 @@
Thy/thy_syn.ML Thy/thy_read.ML Thy/thm_database.ML
#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE)
+$(BIN)/Pure: $(FILES) $(SYNTAX_FILES) $(THY_FILES) $(ML_DBASE)
case "$(COMP)" in \
poly*) echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
- | $(COMP) $(BIN)/Pure;\
+ | $(COMP) $(BIN)/Pure;\
discgarb -c $(BIN)/Pure;;\
sml*) if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
- then echo Bad value for ISABELLEBIN: \
- $(BIN) is not a writable directory; \
- exit 1; \
- fi;\
- echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;' | $(COMP);;\
+ then echo Bad value for ISABELLEBIN: \
+ $(BIN) is not a writable directory; \
+ exit 1; \
+ fi;\
+ echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1; xML"$(BIN)/Pure" banner;' | $(COMP);;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml;;\
esac
test: $(BIN)/Pure
-
-.PRECIOUS: $(BIN)/Pure
+.PRECIOUS: $(BIN)/Pure
--- a/src/Sequents/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/Sequents/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (Sequents) #
+# Makefile for Isabelle (Sequents) #
# #
#########################################################################
@@ -31,39 +31,39 @@
ex/ILL/ILL_kleene_lemmas.ML \
$(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
-$(BIN)/Sequents: $(BIN)/Pure $(FILES)
+$(BIN)/Sequents: $(BIN)/Pure $(FILES)
case "$(COMP)" in \
- poly*) echo 'make_database"$(BIN)/Sequents"; quit();' \
+ 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;\
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml;;\
esac
$(BIN)/Pure:
cd ../Pure; $(MAKE)
-test: $(BIN)/Sequents $(EX_FILES)
+test: $(BIN)/Sequents $(EX_FILES)
case "$(COMP)" in \
poly*) echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\
sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\
*) echo Bad value for ISABELLECOMP: \
- $(COMP) is not poly or sml;;\
+ $(COMP) is not poly or sml;;\
esac
--- a/src/ZF/Makefile Mon Oct 14 11:08:54 1996 +0200
+++ b/src/ZF/Makefile Tue Oct 15 10:46:42 1996 +0200
@@ -1,7 +1,7 @@
# $Id$
#########################################################################
# #
-# Makefile for Isabelle (ZF) #
+# Makefile for Isabelle (ZF) #
# #
#########################################################################
@@ -31,31 +31,31 @@
Zorn Nat Finite List
FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML \
- $(NAMES:%=%.thy) $(NAMES:%=%.ML)
+ $(NAMES:%=%.thy) $(NAMES:%=%.ML)
#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/ZF: $(BIN)/FOL $(FILES)
+$(BIN)/ZF: $(BIN)/FOL $(FILES)
case "$(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;\
+ 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;\
+ 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;;\
+ 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;;\
+ $(COMP) is not poly or sml; exit 1;;\
esac
$(BIN)/FOL:
@@ -68,7 +68,7 @@
poly*) echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
sml*) echo "$ISABELLEBIN/ZF" ;;\
*) echo "echo Bad value for ISABELLECOMP: \
- $ISABELLEBIN is not poly or sml; exit 1" ;;\
+ $ISABELLEBIN is not poly or sml; exit 1" ;;\
esac
##IMP-semantics example
@@ -77,68 +77,68 @@
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
+ 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 Language MT Map Static Types Values
COIND_FILES = Coind/ROOT.ML Coind/BCR.thy Coind/Dynamic.thy \
- $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
+ $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
-Coind: $(BIN)/ZF $(COIND_FILES)
+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
+ 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 OrdQuant Transrec2 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 first recfunAC16 rel_is_fun
+ DC DC_lemmas HH Hartog WO1_AC \
+ WO2_AC16 WO6_WO1 WO_AC first 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/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)
+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
+ 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
+ Cube Residuals Terms
RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) \
- $(RESID_NAMES:%=Resid/%.ML)
+ $(RESID_NAMES:%=Resid/%.ML)
-Resid: $(BIN)/ZF $(RESID_FILES)
+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
+ 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
+ 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)
+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
+ 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
+test: $(BIN)/ZF IMP Coind AC Resid ex
echo 'Test examples ran successfully' > test
.PRECIOUS: $(BIN)/FOL $(BIN)/ZF