--- a/src/CCL/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (CCL) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes FOL if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-
-SET_FILES = ROOT.ML Set.thy Set.ML subset.ML equalities.ML mono.ML \
- 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
-
-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)
- @case `basename "$(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;\
- 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;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-$(BIN)/FOL:
- cd ../FOL; $(MAKE)
-
-test: ex/ROOT.ML $(BIN)/CCL $(EX_FILES)
- @case `basename "$(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;;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/FOL $(BIN)/CCL
--- a/src/CTT/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (CTT) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-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
- @case `basename "$(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;\
- 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;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES)
- @case `basename "$(COMP)"` in \
- poly*) echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CTT ;;\
- sml*) echo 'exit_use_dir"ex";' | $(BIN)/CTT;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/CTT
--- a/src/Cube/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (Cube) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-#WARNING: Poly/ML databases may fail if copied or moved!
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES = ROOT.ML Cube.thy Cube.ML
-
-$(BIN)/Cube: $(BIN)/Pure $(FILES)
- @case `basename "$(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;\
- 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".";' \
- | $(COMP) $(BIN)/Cube;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-test: ex/ROOT.ML ex/ex.ML $(BIN)/Cube
- @case `basename "$(COMP)"` in \
- poly*) echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/Cube ;;\
- sml*) echo 'exit_use_dir"ex";' | $(BIN)/Cube;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/Cube
--- a/src/FOL/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (FOL) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-FILES = ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
- thy_data.ML cladata.ML \
- ../Provers/hypsubst.ML ../Provers/classical.ML ../Provers/blast.ML \
- ../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.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 ];\
- then echo Bad value for ISABELLEBIN: \
- $(BIN) is the Isabelle source directory; \
- exit 1; \
- fi
- @case `basename "$(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;\
- 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;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-test: ex/ROOT.ML $(BIN)/FOL $(EX_FILES)
- @case `basename "$(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;;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/FOL
--- a/src/FOLP/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (FOLP) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-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\
- ex/intro.ML ex/Nat.ML ex/Nat.thy ex/Prolog.ML ex/Prolog.thy\
- ex/prop.ML ex/quant.ML
-
-$(BIN)/FOLP: $(BIN)/Pure $(FILES)
- @case `basename "$(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;\
- 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".";' \
- | $(COMP) $(BIN)/FOLP;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-test: ex/ROOT.ML $(BIN)/FOLP $(EX_FILES)
- @case `basename "$(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;;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/FOLP
--- a/src/HOL/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,225 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (HOL) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes pure Isabelle (Pure) if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-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
-
-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/blast.ML \
- ../Provers/simplifier.ML ../Provers/splitter.ML\
- ../Provers/nat_transitive.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
- @case `basename "$(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;\
- 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;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml; exit 1;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-#### Testing of HOL
-
-#A macro referring to the object-logic (depends on ML compiler)
-# [Thanks to Thomas Santen and Stephan Herrmann from GMD First]
-LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
- poly*) echo "$(ISABELLECOMP) $(ISABELLEBIN)/HOL" ;;\
- sml*) echo "$(ISABELLEBIN)/HOL" ;;\
- *) echo "echo; echo Bad value for ISABELLECOMP: \
- $(ISABELLECOMP) is not poly or sml; exit 1" ;;\
- esac`
-
-
-## Inductive definitions: simple examples
-
-INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
-
-INDUCT_FILES = Induct/ROOT.ML \
- $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
-
-Induct: $(BIN)/HOL $(INDUCT_FILES)
- @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'make_html := true; exit_use_dir"Induct";quit();' | $(LOGIC); \
- else echo 'exit_use_dir"Induct";quit();' | $(LOGIC); \
- fi
-
-
-##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)
- @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
-
-##Hoare logic
-Hoare_NAMES = Hoare Arith2 Examples
-Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
- $(Hoare_NAMES:%=Hoare/%.ML)
-
-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
-
-##The integers in HOL
-INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
-
-INTEG_FILES = Integ/ROOT.ML \
- $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
-
-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
-
-
-##Authentication & Security Protocols
-Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
- Recur WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public
-
-AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
-
-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
-
-
-##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: $(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
-
-##Confluence of Lambda-calculus
-LAMBDA_NAMES = Lambda ParRed Commutation Eta
-
-LAMBDA_FILES = Lambda/ROOT.ML \
- $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
-
-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
-
-## Type inference without let
-
-W0_NAMES = I Maybe MiniML Type W
-
-W0_FILES = W0/ROOT.ML \
- $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
-
-W0: $(BIN)/HOL $(W0_FILES)
- @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
- then echo 'make_html := true; exit_use_dir"W0";quit();' \
- | $(LOGIC);\
- else echo 'exit_use_dir"W0";quit();' | $(LOGIC); \
- fi
-
-## Type inference with let
-
-MINIML_NAMES = Generalize Instance Maybe MiniML Type W
-
-MINIML_FILES = MiniML/ROOT.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
-
-##Lexical analysis
-LEX_FILES = Auto AutoChopper Chopper Prefix
-
-LEX_FILES = Lex/ROOT.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
-
-##Miscellaneous examples
-EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum 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: $(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
-
-#Full test.
-test: $(BIN)/HOL \
- Induct IMP Hoare Lex Integ Auth Subst Lambda \
- W0 MiniML IOA AxClasses Quot ex
- echo 'Test examples ran successfully' > test
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
--- a/src/HOLCF/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-# $Id$
-############################################################################
-# #
-# Makefile for Isabelle (HOLCF) #
-# #
-############################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes HOL Isabelle if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-THYS = Porder.thy Porder0.thy Pcpo.thy \
- Fun1.thy Fun2.thy Fun3.thy \
- Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
- Cprod1.thy Cprod2.thy Cprod3.thy \
- Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
- Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
- Up1.thy Up2.thy Up3.thy Fix.thy \
- One.thy Tr.thy \
- Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
-
-ONLYTHYS =
-
-FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
- ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
- ax_ops/thy_ops.ML ax_ops/thy_syntax.ML \
- domain/library.ML domain/syntax.ML domain/axioms.ML \
- domain/theorems.ML domain/extender.ML domain/interface.ML
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/HOLCF: $(BIN)/HOL $(FILES)
- @case `basename "$(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;\
- 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".";' \
- | $(COMP) $(BIN)/HOLCF;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-$(BIN)/HOL:
- cd ../HOL; $(MAKE)
-
-EX_THYS = ex/Classlib.thy\
- ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
- ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
- ex/Hoare.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)
- @case `basename "$(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;;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF
-
--- a/src/LCF/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (LCF) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes FOL if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-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 `basename "$(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;\
- 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;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-(BIN)/FOL:
- cd ../FOL; $(MAKE)
-
-test: ex/ROOT.ML ex/ex.ML $(BIN)/LCF
- @case `basename "$(COMP)"` in \
- poly*) echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/LCF ;;\
- sml*) echo 'exit_use_dir"ex";' | $(BIN)/LCF;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-.PRECIOUS: $(BIN)/FOL $(BIN)/LCF
--- a/src/Sequents/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (Sequents) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes Pure if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-NAMES = ILL LK S4 S43 T
-FILES = ROOT.ML Sequents.thy prover.ML $(NAMES:%=%.thy) $(NAMES:%=%.ML)
-
-ILL_NAMES = ILL_predlog washing
-EX_FILES = ex/ROOT.ML \
- ex/LK/ROOT.ML ex/LK/hardquant.ML ex/LK/prop.ML ex/LK/quant.ML \
- ex/Modal/ROOT.ML ex/Modal/S43thms.ML ex/Modal/S4thms.ML ex/Modal/Tthms.ML \
- ex/ILL/ILL_kleene_lemmas.ML \
- $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
-
-$(BIN)/Sequents: $(BIN)/Pure $(FILES)
- @case `basename "$(COMP)"` in \
- 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;\
- 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;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-$(BIN)/Pure:
- cd ../Pure; $(MAKE)
-
-test: $(BIN)/Sequents $(EX_FILES)
- @case `basename "$(COMP)"` in \
- poly*) echo 'exit_use_dir"ex";quit();' | $(COMP) $(BIN)/Sequents;;\
- sml*) echo 'exit_use_dir"ex";' | $(BIN)/Sequents;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml;;\
- esac
-
-
-.PRECIOUS: $(BIN)/Pure $(BIN)/Sequents
--- a/src/ZF/Makefile Fri Jun 20 11:19:39 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-# $Id$
-#########################################################################
-# #
-# Makefile for Isabelle (ZF) #
-# #
-#########################################################################
-
-#To make the system, cd to this directory and type
-# make
-#To make the system and test it on standard examples, type
-# make test
-#To generate HTML files for every theory, set the environment variable
-#MAKE_HTML or add the parameter "MAKE_HTML=".
-
-#Environment variable ISABELLECOMP specifies the compiler.
-#Environment variable ISABELLEBIN specifies the destination directory.
-#For Poly/ML, ISABELLEBIN must begin with a /
-
-#Makes FOL if this file is ABSENT -- but not
-#if it is out of date, since this Makefile does not know its dependencies!
-
-BIN = $(ISABELLEBIN)
-COMP = $(ISABELLECOMP)
-NAMES = ZF upair subset pair domrange \
- func AC equalities Bool \
- Sum QPair mono Fixedpt ind_syntax cartprod add_ind_def \
- constructor intr_elim indrule Inductive Perm Rel EquivClass Trancl \
- WF Order Ordinal Epsilon Arith Univ \
- QUniv Datatype OrderArith OrderType \
- Cardinal CardinalArith Cardinal_AC InfDatatype \
- Zorn Nat Finite List
-
-FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML simpdata.ML typechk.ML\
- $(NAMES:%=%.thy) $(NAMES:%=%.ML)
-
-#Uses cp rather than make_database because Poly/ML allows only 3 levels
-$(BIN)/ZF: $(BIN)/FOL $(FILES)
- @case `basename "$(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;\
- 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;\
- 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;;\
- *) echo Bad value for ISABELLECOMP: \
- \"$(COMP)\" is not poly or sml; exit 1;;\
- esac
-
-$(BIN)/FOL:
- cd ../FOL; $(MAKE)
-
-#### Testing of ZF
-
-#A macro referring to the object-logic (depends on ML compiler)
-# [Thanks to Thomas Santen and Stephan Herrmann from GMD First]
-LOGIC=`case \`basename "$(ISABELLECOMP)"\` in \
- poly*) echo "$(ISABELLECOMP) $(ISABELLEBIN)/ZF" ;;\
- sml*) echo "$(ISABELLEBIN)/ZF" ;;\
- *) echo "echo; echo Bad value for ISABELLECOMP: \
- $(ISABELLECOMP) is not poly or sml; exit 1" ;;\
- esac`
-
-##IMP-semantics example
-IMP_NAMES = Com Denotation Equiv
-IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
-
-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
-
-##Coinduction example
-COIND_NAMES = ECR MT Map Static Types Values
-
-COIND_FILES = Coind/ROOT.ML Coind/Language.thy Coind/BCR.thy Coind/Dynamic.thy\
- $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
-
-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
-
-##AC examples
-AC_NAMES = AC_Equiv 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 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: $(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
-
-##Residuals example
-
-RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
- Cube Residuals Terms
-
-RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) \
- $(RESID_NAMES:%=Resid/%.ML)
-
-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
-
-##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
-
-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)
- @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
-
-#Full test.
-test: $(BIN)/ZF IMP Coind AC Resid ex
- echo 'Test examples ran successfully' > test
-
-.PRECIOUS: $(BIN)/FOL $(BIN)/ZF