# HG changeset patch # User paulson # Date 845369202 -7200 # Node ID 2061df98aab5cf6a699510b992b7c8dc8cf28424 # Parent 8e3e56fecfbe30a2697b545becce7e629cd6c910 Removed extraneous spaces from all Makefiles diff -r 8e3e56fecfbe -r 2061df98aab5 src/CCL/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/CTT/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/Cube/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/FOL/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/FOLP/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/HOL/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/HOLCF/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/LCF/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/Pure/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/Sequents/Makefile --- 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 diff -r 8e3e56fecfbe -r 2061df98aab5 src/ZF/Makefile --- 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