Removed extraneous spaces from all Makefiles
authorpaulson
Tue Oct 15 10:46:42 1996 +0200 (1996-10-15)
changeset 20942061df98aab5
parent 2093 8e3e56fecfbe
child 2095 e8544d73a7aa
Removed extraneous spaces from all Makefiles
src/CCL/Makefile
src/CTT/Makefile
src/Cube/Makefile
src/FOL/Makefile
src/FOLP/Makefile
src/HOL/Makefile
src/HOLCF/Makefile
src/LCF/Makefile
src/Pure/Makefile
src/Sequents/Makefile
src/ZF/Makefile
     1.1 --- a/src/CCL/Makefile	Mon Oct 14 11:08:54 1996 +0200
     1.2 +++ b/src/CCL/Makefile	Tue Oct 15 10:46:42 1996 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  # $Id$
     1.5  #########################################################################
     1.6  #									#
     1.7 -# 			Makefile for Isabelle (CCL)			#
     1.8 +#			Makefile for Isabelle (CCL)			#
     1.9  #									#
    1.10  #########################################################################
    1.11  
    1.12 @@ -26,54 +26,54 @@
    1.13  	    Gfp.thy Gfp.ML Lfp.thy Lfp.ML
    1.14  
    1.15  CCL_FILES = CCL.thy CCL.ML Term.thy Term.ML Type.thy Type.ML \
    1.16 -            coinduction.ML Hered.thy Hered.ML Trancl.thy Trancl.ML\
    1.17 -            Wfd.thy Wfd.ML genrec.ML typecheck.ML eval.ML Fix.thy Fix.ML
    1.18 +	    coinduction.ML Hered.thy Hered.ML Trancl.thy Trancl.ML\
    1.19 +	    Wfd.thy Wfd.ML genrec.ML typecheck.ML eval.ML Fix.thy Fix.ML
    1.20  
    1.21  EX_FILES = ex/ROOT.ML ex/Flag.ML ex/Flag.thy ex/List.ML ex/List.thy\
    1.22  	   ex/Nat.ML ex/Nat.thy ex/Stream.ML ex/Stream.thy
    1.23  
    1.24  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    1.25 -$(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)  $(CCL_FILES) 
    1.26 +$(BIN)/CCL:   $(BIN)/FOL  $(SET_FILES)	$(CCL_FILES) 
    1.27  	case "$(COMP)" in \
    1.28  	poly*)	cp $(BIN)/FOL $(BIN)/CCL;\
    1.29 -                if [ "$${MAKE_HTML}" = "true" ]; \
    1.30 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    1.31 -                       | $(COMP) $(BIN)/CCL;\
    1.32 +		if [ "$${MAKE_HTML}" = "true" ]; \
    1.33 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    1.34 +		       | $(COMP) $(BIN)/CCL;\
    1.35  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.36 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CCL;\
    1.37 -                else echo 'open PolyML; exit_use_dir".";' \
    1.38 -                       | $(COMP) $(BIN)/CCL;\
    1.39 -                fi;\
    1.40 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/CCL;\
    1.41 +		else echo 'open PolyML; exit_use_dir".";' \
    1.42 +		       | $(COMP) $(BIN)/CCL;\
    1.43 +		fi;\
    1.44  		discgarb -c $(BIN)/CCL;;\
    1.45 -	sml*)   if [ "$${MAKE_HTML}" = "true" ]; \
    1.46 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
    1.47 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.48 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/CCL" banner;' \
    1.49 -                       | $(BIN)/FOL;\
    1.50 -                else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
    1.51 -                       | $(BIN)/FOL;\
    1.52 -                fi;;\
    1.53 +	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    1.54 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/CCL" banner;' | $(BIN)/FOL;\
    1.55 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    1.56 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/CCL" banner;' \
    1.57 +		       | $(BIN)/FOL;\
    1.58 +		else echo 'exit_use_dir"."; xML"$(BIN)/CCL" banner;' \
    1.59 +		       | $(BIN)/FOL;\
    1.60 +		fi;;\
    1.61  	*)	echo Bad value for ISABELLECOMP: \
    1.62 -                	$(COMP) is not poly or sml;;\
    1.63 +			$(COMP) is not poly or sml;;\
    1.64  	esac
    1.65  
    1.66  $(BIN)/FOL:
    1.67  	cd ../FOL;  $(MAKE)
    1.68  
    1.69 -test:   ex/ROOT.ML  $(BIN)/CCL  $(EX_FILES)
    1.70 +test:	ex/ROOT.ML  $(BIN)/CCL	$(EX_FILES)
    1.71  	case "$(COMP)" in \
    1.72  	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.73 -                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    1.74 -                       | $(COMP) $(BIN)/CCL;\
    1.75 -                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CCL;\
    1.76 -                fi;;\
    1.77 +		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    1.78 +		       | $(COMP) $(BIN)/CCL;\
    1.79 +		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CCL;\
    1.80 +		fi;;\
    1.81  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.82 -                then echo 'make_html := true; exit_use_dir"ex";' \
    1.83 -                       | $(BIN)/CCL;\
    1.84 -                else echo 'exit_use_dir"ex";' | $(BIN)/CCL;\
    1.85 -                fi;;\
    1.86 +		then echo 'make_html := true; exit_use_dir"ex";' \
    1.87 +		       | $(BIN)/CCL;\
    1.88 +		else echo 'exit_use_dir"ex";' | $(BIN)/CCL;\
    1.89 +		fi;;\
    1.90  	*)	echo Bad value for ISABELLECOMP: \
    1.91 -                	$(COMP) is not poly or sml;;\
    1.92 +			$(COMP) is not poly or sml;;\
    1.93  	esac
    1.94  
    1.95  .PRECIOUS:  $(BIN)/FOL $(BIN)/CCL 
     2.1 --- a/src/CTT/Makefile	Mon Oct 14 11:08:54 1996 +0200
     2.2 +++ b/src/CTT/Makefile	Tue Oct 15 10:46:42 1996 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  # $Id$
     2.5  #########################################################################
     2.6  #									#
     2.7 -# 			Makefile for Isabelle (CTT)			#
     2.8 +#			Makefile for Isabelle (CTT)			#
     2.9  #									#
    2.10  #########################################################################
    2.11  
    2.12 @@ -21,50 +21,50 @@
    2.13  
    2.14  BIN = $(ISABELLEBIN)
    2.15  COMP = $(ISABELLECOMP)
    2.16 -FILES = 	ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
    2.17 +FILES =		ROOT.ML CTT.thy CTT.ML Bool.thy Bool.ML \
    2.18  		Arith.thy Arith.ML rew.ML ../Provers/typedsimp.ML
    2.19  
    2.20  EX_FILES = ex/ROOT.ML ex/elim.ML ex/equal.ML ex/synth.ML ex/typechk.ML
    2.21  
    2.22  $(BIN)/CTT:   $(BIN)/Pure  $(FILES) 
    2.23  	if [ -d $${ISABELLEBIN:?}/Pure ];\
    2.24 -           	then echo Bad value for ISABELLEBIN: \
    2.25 -                	$(BIN) is the Isabelle source directory; \
    2.26 -                	exit 1; \
    2.27 -           	fi;\
    2.28 +		then echo Bad value for ISABELLEBIN: \
    2.29 +			$(BIN) is the Isabelle source directory; \
    2.30 +			exit 1; \
    2.31 +		fi;\
    2.32  	case "$(COMP)" in \
    2.33  	poly*)	echo 'make_database"$(BIN)/CTT"; quit();'  \
    2.34  			| $(COMP) $(BIN)/Pure;\
    2.35 -                if [ "$${MAKE_HTML}" = "true" ]; \
    2.36 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    2.37 -                       | $(COMP) $(BIN)/CTT;\
    2.38 +		if [ "$${MAKE_HTML}" = "true" ]; \
    2.39 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    2.40 +		       | $(COMP) $(BIN)/CTT;\
    2.41  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    2.42 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/CTT;\
    2.43 -                else echo 'open PolyML; exit_use_dir".";' \
    2.44 -                       | $(COMP) $(BIN)/CTT;\
    2.45 -                fi;\
    2.46 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/CTT;\
    2.47 +		else echo 'open PolyML; exit_use_dir".";' \
    2.48 +		       | $(COMP) $(BIN)/CTT;\
    2.49 +		fi;\
    2.50  		discgarb -c $(BIN)/CTT;;\
    2.51  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    2.52 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
    2.53 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    2.54 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/CTT" banner;' \
    2.55 -                       | $(BIN)/Pure;\
    2.56 -                else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
    2.57 -                       | $(BIN)/Pure;\
    2.58 -                fi;;\
    2.59 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/CTT" banner;' | $(BIN)/Pure;\
    2.60 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    2.61 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/CTT" banner;' \
    2.62 +		       | $(BIN)/Pure;\
    2.63 +		else echo 'exit_use_dir"."; xML"$(BIN)/CTT" banner;' \
    2.64 +		       | $(BIN)/Pure;\
    2.65 +		fi;;\
    2.66  	*)	echo Bad value for ISABELLECOMP: \
    2.67 -                	$(COMP) is not poly or sml;;\
    2.68 +			$(COMP) is not poly or sml;;\
    2.69  	esac
    2.70  
    2.71  $(BIN)/Pure:
    2.72  	cd ../Pure;  $(MAKE)
    2.73  
    2.74 -test:   ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
    2.75 +test:	ex/ROOT.ML $(BIN)/CTT  $(EX_FILES) 
    2.76  	case "$(COMP)" in \
    2.77  	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
    2.78  	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\
    2.79  	*)	echo Bad value for ISABELLECOMP: \
    2.80 -                	$(COMP) is not poly or sml;;\
    2.81 +			$(COMP) is not poly or sml;;\
    2.82  	esac
    2.83  
    2.84 -.PRECIOUS:  $(BIN)/Pure  $(BIN)/CTT 
    2.85 +.PRECIOUS:  $(BIN)/Pure	 $(BIN)/CTT 
     3.1 --- a/src/Cube/Makefile	Mon Oct 14 11:08:54 1996 +0200
     3.2 +++ b/src/Cube/Makefile	Tue Oct 15 10:46:42 1996 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  # $Id$
     3.5  #########################################################################
     3.6  #									#
     3.7 -# 			Makefile for Isabelle (Cube)			#
     3.8 +#			Makefile for Isabelle (Cube)			#
     3.9  #									#
    3.10  #########################################################################
    3.11  
    3.12 @@ -22,42 +22,42 @@
    3.13  
    3.14  BIN = $(ISABELLEBIN)
    3.15  COMP = $(ISABELLECOMP)
    3.16 -FILES = 	ROOT.ML  Cube.thy  Cube.ML
    3.17 +FILES =		ROOT.ML	 Cube.thy  Cube.ML
    3.18  
    3.19  $(BIN)/Cube:   $(BIN)/Pure  $(FILES) 
    3.20  	case "$(COMP)" in \
    3.21  	poly*)	echo 'make_database"$(BIN)/Cube"; quit();'  \
    3.22  			| $(COMP) $(BIN)/Pure;\
    3.23 -                if [ "$${MAKE_HTML}" = "true" ]; \
    3.24 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    3.25 -                       | $(COMP) $(BIN)/Cube;\
    3.26 +		if [ "$${MAKE_HTML}" = "true" ]; \
    3.27 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    3.28 +		       | $(COMP) $(BIN)/Cube;\
    3.29  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    3.30 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Cube;\
    3.31 -                else echo 'open PolyML; exit_use_dir".";' \
    3.32 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/Cube;\
    3.33 +		else echo 'open PolyML; exit_use_dir".";' \
    3.34  		       | $(COMP) $(BIN)/Cube;\
    3.35 -                fi;\
    3.36 +		fi;\
    3.37  		discgarb -c $(BIN)/Cube;;\
    3.38  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    3.39 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
    3.40 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    3.41 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Cube" banner;' \
    3.42 -                       | $(BIN)/Pure;\
    3.43 -                else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
    3.44 -                       | $(BIN)/Pure;\
    3.45 -                fi;;\
    3.46 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/Cube" banner;' | $(BIN)/Pure;\
    3.47 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    3.48 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/Cube" banner;' \
    3.49 +		       | $(BIN)/Pure;\
    3.50 +		else echo 'exit_use_dir"."; xML"$(BIN)/Cube" banner;' \
    3.51 +		       | $(BIN)/Pure;\
    3.52 +		fi;;\
    3.53  	*)	echo Bad value for ISABELLECOMP: \
    3.54 -                	$(COMP) is not poly or sml;;\
    3.55 +			$(COMP) is not poly or sml;;\
    3.56  	esac
    3.57  
    3.58  $(BIN)/Pure:
    3.59  	cd ../Pure;  $(MAKE)
    3.60  
    3.61 -test:   ex.ML $(BIN)/Cube
    3.62 +test:	ex.ML $(BIN)/Cube
    3.63  	case "$(COMP)" in \
    3.64  	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/Cube ;;\
    3.65  	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/Cube;;\
    3.66  	*)	echo Bad value for ISABELLECOMP: \
    3.67 -                	$(COMP) is not poly or sml;;\
    3.68 +			$(COMP) is not poly or sml;;\
    3.69  	esac
    3.70  
    3.71 -.PRECIOUS:  $(BIN)/Pure  $(BIN)/Cube 
    3.72 +.PRECIOUS:  $(BIN)/Pure	 $(BIN)/Cube 
     4.1 --- a/src/FOL/Makefile	Mon Oct 14 11:08:54 1996 +0200
     4.2 +++ b/src/FOL/Makefile	Tue Oct 15 10:46:42 1996 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  # $Id$
     4.5  #########################################################################
     4.6  #									#
     4.7 -# 			Makefile for Isabelle (FOL)			#
     4.8 +#			Makefile for Isabelle (FOL)			#
     4.9  #									#
    4.10  #########################################################################
    4.11  
    4.12 @@ -21,7 +21,7 @@
    4.13  
    4.14  BIN = $(ISABELLEBIN)
    4.15  COMP = $(ISABELLECOMP)
    4.16 -FILES =  ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    4.17 +FILES =	 ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
    4.18  	 ../Provers/hypsubst.ML ../Provers/classical.ML \
    4.19  	 ../Provers/simplifier.ML ../Provers/splitter.ML ../Provers/ind.ML
    4.20  
    4.21 @@ -31,51 +31,51 @@
    4.22  
    4.23  $(BIN)/FOL:   $(BIN)/Pure  $(FILES) 
    4.24  	if [ -d $${ISABELLEBIN:?}/Pure ];\
    4.25 -           	then echo Bad value for ISABELLEBIN: \
    4.26 -                	$(BIN) is the Isabelle source directory; \
    4.27 -                	exit 1; \
    4.28 -           	fi;\
    4.29 +		then echo Bad value for ISABELLEBIN: \
    4.30 +			$(BIN) is the Isabelle source directory; \
    4.31 +			exit 1; \
    4.32 +		fi;\
    4.33  	case "$(COMP)" in \
    4.34  	poly*)	echo 'make_database"$(BIN)/FOL"; quit();' \
    4.35  		  | $(COMP) $(BIN)/Pure;\
    4.36 -                if [ "$${MAKE_HTML}" = "true" ]; \
    4.37 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    4.38 -                       | $(COMP) $(BIN)/FOL;\
    4.39 +		if [ "$${MAKE_HTML}" = "true" ]; \
    4.40 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    4.41 +		       | $(COMP) $(BIN)/FOL;\
    4.42  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.43 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOL;\
    4.44 -                else echo 'open PolyML; exit_use_dir".";' \
    4.45 -                       | $(COMP) $(BIN)/FOL;\
    4.46 -                fi;\
    4.47 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/FOL;\
    4.48 +		else echo 'open PolyML; exit_use_dir".";' \
    4.49 +		       | $(COMP) $(BIN)/FOL;\
    4.50 +		fi;\
    4.51  		discgarb -c $(BIN)/FOL;;\
    4.52  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    4.53 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
    4.54 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    4.55 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/FOL" banner;' \
    4.56 -                       | $(BIN)/Pure;\
    4.57 -                else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \
    4.58 -                       | $(BIN)/Pure;\
    4.59 -                fi;;\
    4.60 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/FOL" banner;' | $(BIN)/Pure;\
    4.61 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    4.62 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/FOL" banner;' \
    4.63 +		       | $(BIN)/Pure;\
    4.64 +		else echo 'exit_use_dir"."; xML"$(BIN)/FOL" banner;' \
    4.65 +		       | $(BIN)/Pure;\
    4.66 +		fi;;\
    4.67  	*)	echo Bad value for ISABELLECOMP: \
    4.68 -                	$(COMP) is not poly or sml;;\
    4.69 +			$(COMP) is not poly or sml;;\
    4.70  	esac
    4.71  
    4.72  $(BIN)/Pure:
    4.73  	cd ../Pure;  $(MAKE)
    4.74  
    4.75 -test:   ex/ROOT.ML  $(BIN)/FOL  $(EX_FILES) 
    4.76 +test:	ex/ROOT.ML  $(BIN)/FOL	$(EX_FILES) 
    4.77  	case "$(COMP)" in \
    4.78 -	poly*)  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.79 -                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    4.80 -                       | $(COMP) $(BIN)/FOL;\
    4.81 -                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\
    4.82 -                fi;;\
    4.83 +	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.84 +		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    4.85 +		       | $(COMP) $(BIN)/FOL;\
    4.86 +		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL;\
    4.87 +		fi;;\
    4.88  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    4.89 -                then echo 'make_html := true; exit_use_dir"ex";' \
    4.90 -                       | $(BIN)/FOL;\
    4.91 -                else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
    4.92 -                fi;;\
    4.93 +		then echo 'make_html := true; exit_use_dir"ex";' \
    4.94 +		       | $(BIN)/FOL;\
    4.95 +		else echo 'exit_use_dir"ex";' | $(BIN)/FOL;\
    4.96 +		fi;;\
    4.97  	*)	echo Bad value for ISABELLECOMP: \
    4.98 -                	$(COMP) is not poly or sml;;\
    4.99 +			$(COMP) is not poly or sml;;\
   4.100  	esac
   4.101  
   4.102  .PRECIOUS:   $(BIN)/Pure  $(BIN)/FOL 
     5.1 --- a/src/FOLP/Makefile	Mon Oct 14 11:08:54 1996 +0200
     5.2 +++ b/src/FOLP/Makefile	Tue Oct 15 10:46:42 1996 +0200
     5.3 @@ -1,7 +1,7 @@
     5.4  #  $Id$
     5.5  #########################################################################
     5.6  #									#
     5.7 -# 			Makefile for Isabelle (FOLP)			#
     5.8 +#			Makefile for Isabelle (FOLP)			#
     5.9  #									#
    5.10  #########################################################################
    5.11  
    5.12 @@ -21,7 +21,7 @@
    5.13  
    5.14  BIN = $(ISABELLEBIN)
    5.15  COMP = $(ISABELLECOMP)
    5.16 -FILES =  ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML\
    5.17 +FILES =	 ROOT.ML IFOLP.thy IFOLP.ML FOLP.thy FOLP.ML intprover.ML simpdata.ML\
    5.18  	 hypsubst.ML classical.ML simp.ML 
    5.19  
    5.20  EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/If.ML ex/If.thy ex/int.ML\
    5.21 @@ -32,44 +32,44 @@
    5.22  	case "$(COMP)" in \
    5.23  	poly*)	echo 'make_database"$(BIN)/FOLP"; quit();'  \
    5.24  			| $(COMP) $(BIN)/Pure;\
    5.25 -                if [ "$${MAKE_HTML}" = "true" ]; \
    5.26 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    5.27 -                       | $(COMP) $(BIN)/FOLP;\
    5.28 +		if [ "$${MAKE_HTML}" = "true" ]; \
    5.29 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    5.30 +		       | $(COMP) $(BIN)/FOLP;\
    5.31  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.32 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/FOLP;\
    5.33 -                else echo 'open PolyML; exit_use_dir".";' \
    5.34 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/FOLP;\
    5.35 +		else echo 'open PolyML; exit_use_dir".";' \
    5.36  		       | $(COMP) $(BIN)/FOLP;\
    5.37 -                fi;\
    5.38 +		fi;\
    5.39  		discgarb -c $(BIN)/FOLP;;\
    5.40  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    5.41 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
    5.42 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    5.43 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/FOLP" banner;' \
    5.44 -                       | $(BIN)/Pure;\
    5.45 -                else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
    5.46 -                       | $(BIN)/Pure;\
    5.47 -                fi;;\
    5.48 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/FOLP" banner;' | $(BIN)/Pure;\
    5.49 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    5.50 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/FOLP" banner;' \
    5.51 +		       | $(BIN)/Pure;\
    5.52 +		else echo 'exit_use_dir"."; xML"$(BIN)/FOLP" banner;' \
    5.53 +		       | $(BIN)/Pure;\
    5.54 +		fi;;\
    5.55  	*)	echo Bad value for ISABELLECOMP: \
    5.56 -                	$(COMP) is not poly or sml;;\
    5.57 +			$(COMP) is not poly or sml;;\
    5.58  	esac
    5.59  
    5.60  $(BIN)/Pure:
    5.61  	cd ../Pure;  $(MAKE)
    5.62  
    5.63 -test:   ex/ROOT.ML  $(BIN)/FOLP  $(EX_FILES) 
    5.64 +test:	ex/ROOT.ML  $(BIN)/FOLP	 $(EX_FILES) 
    5.65  	case "$(COMP)" in \
    5.66 -	poly*)  if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.67 -                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    5.68 -                       | $(COMP) $(BIN)/FOLP;\
    5.69 -                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\
    5.70 -                fi;;\
    5.71 +	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.72 +		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    5.73 +		       | $(COMP) $(BIN)/FOLP;\
    5.74 +		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP;\
    5.75 +		fi;;\
    5.76  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    5.77 -                then echo 'make_html := true; exit_use_dir"ex";' \
    5.78 -                       | $(BIN)/FOLP;\
    5.79 -                else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
    5.80 -                fi;;\
    5.81 +		then echo 'make_html := true; exit_use_dir"ex";' \
    5.82 +		       | $(BIN)/FOLP;\
    5.83 +		else echo 'exit_use_dir"ex";' | $(BIN)/FOLP;\
    5.84 +		fi;;\
    5.85  	*)	echo Bad value for ISABELLECOMP: \
    5.86 -                	$(COMP) is not poly or sml;;\
    5.87 +			$(COMP) is not poly or sml;;\
    5.88  	esac
    5.89  
    5.90  .PRECIOUS:   $(BIN)/Pure  $(BIN)/FOLP 
     6.1 --- a/src/HOL/Makefile	Mon Oct 14 11:08:54 1996 +0200
     6.2 +++ b/src/HOL/Makefile	Tue Oct 15 10:46:42 1996 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  # $Id$
     6.5  #########################################################################
     6.6  #									#
     6.7 -# 			Makefile for Isabelle (HOL)			#
     6.8 +#			Makefile for Isabelle (HOL)			#
     6.9  #									#
    6.10  #########################################################################
    6.11  
    6.12 @@ -22,44 +22,44 @@
    6.13  BIN = $(ISABELLEBIN)
    6.14  COMP = $(ISABELLECOMP)
    6.15  NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF \
    6.16 -        mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
    6.17 -        Sexp Univ List RelPow Option
    6.18 +	mono Lfp Gfp Nat intr_elim indrule Inductive Finite Arith \
    6.19 +	Sexp Univ List RelPow Option
    6.20  
    6.21  FILES = ROOT.ML add_ind_def.ML datatype.ML hologic.ML\
    6.22  	ind_syntax.ML cladata.ML simpdata.ML\
    6.23  	typedef.ML thy_syntax.ML thy_data.ML ../Pure/section_utils.ML\
    6.24  	../Provers/hypsubst.ML ../Provers/classical.ML\
    6.25 -        ../Provers/simplifier.ML ../Provers/splitter.ML\
    6.26 - 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    6.27 +	../Provers/simplifier.ML ../Provers/splitter.ML\
    6.28 +	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
    6.29  
    6.30  $(BIN)/HOL:   $(BIN)/Pure  $(FILES) 
    6.31  	if [ -d $${ISABELLEBIN:?}/Pure ];\
    6.32 -           	then echo Bad value for ISABELLEBIN: \
    6.33 -                	$(BIN) is the Isabelle source directory; \
    6.34 -                	exit 1; \
    6.35 -           	fi;\
    6.36 +		then echo Bad value for ISABELLEBIN: \
    6.37 +			$(BIN) is the Isabelle source directory; \
    6.38 +			exit 1; \
    6.39 +		fi;\
    6.40  	case "$(COMP)" in \
    6.41  	poly*)	echo 'make_database"$(BIN)/HOL"; quit();'  \
    6.42  		  | $(COMP) $(BIN)/Pure;\
    6.43 -                if [ "$${MAKE_HTML}" = "true" ]; \
    6.44 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    6.45 -                       | $(COMP) $(BIN)/HOL;\
    6.46 +		if [ "$${MAKE_HTML}" = "true" ]; \
    6.47 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    6.48 +		       | $(COMP) $(BIN)/HOL;\
    6.49  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.50 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOL;\
    6.51 -                else echo 'open PolyML; exit_use_dir".";' \
    6.52 -                       | $(COMP) $(BIN)/HOL;\
    6.53 -                fi;\
    6.54 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/HOL;\
    6.55 +		else echo 'open PolyML; exit_use_dir".";' \
    6.56 +		       | $(COMP) $(BIN)/HOL;\
    6.57 +		fi;\
    6.58  		discgarb -c $(BIN)/HOL;;\
    6.59  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    6.60 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    6.61 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    6.62 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/HOL" banner;' \
    6.63 -                       | $(BIN)/Pure;\
    6.64 -                else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
    6.65 -                       | $(BIN)/Pure;\
    6.66 -                fi;;\
    6.67 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/HOL" banner;' | $(BIN)/Pure;\
    6.68 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    6.69 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/HOL" banner;' \
    6.70 +		       | $(BIN)/Pure;\
    6.71 +		else echo 'exit_use_dir"."; xML"$(BIN)/HOL" banner;' \
    6.72 +		       | $(BIN)/Pure;\
    6.73 +		fi;;\
    6.74  	*)	echo Bad value for ISABELLECOMP: \
    6.75 -                	$(COMP) is not poly or sml; exit 1;;\
    6.76 +			$(COMP) is not poly or sml; exit 1;;\
    6.77  	esac
    6.78  
    6.79  $(BIN)/Pure:
    6.80 @@ -72,45 +72,45 @@
    6.81  	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
    6.82  	sml*)	echo "$ISABELLEBIN/HOL" ;;\
    6.83  	*)	echo "echo Bad value for ISABELLECOMP: \
    6.84 -                	$ISABELLEBIN is not poly or sml; exit 1" ;;\
    6.85 +			$ISABELLEBIN is not poly or sml; exit 1" ;;\
    6.86  	esac
    6.87  
    6.88  ##IMP-semantics example
    6.89  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    6.90  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    6.91  
    6.92 -IMP:    $(BIN)/HOL  $(IMP_FILES)
    6.93 +IMP:	$(BIN)/HOL  $(IMP_FILES)
    6.94  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    6.95 -        then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
    6.96 -        else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
    6.97 -        fi
    6.98 +	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
    6.99 +	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
   6.100 +	fi
   6.101  
   6.102  ##Hoare logic
   6.103  Hoare_NAMES = Hoare Arith2 Examples
   6.104  Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
   6.105 -              $(Hoare_NAMES:%=Hoare/%.ML)
   6.106 +	      $(Hoare_NAMES:%=Hoare/%.ML)
   6.107  
   6.108 -Hoare:  $(BIN)/HOL  $(Hoare_FILES)
   6.109 +Hoare:	$(BIN)/HOL  $(Hoare_FILES)
   6.110  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.111 -        then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
   6.112 -        else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
   6.113 -        fi
   6.114 +	then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
   6.115 +	else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
   6.116 +	fi
   6.117  
   6.118  ##The integers in HOL
   6.119  INTEG_NAMES = Equiv Integ 
   6.120  
   6.121  INTEG_FILES = Integ/ROOT.ML \
   6.122 -              $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
   6.123 +	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
   6.124  
   6.125 -Integ:  $(BIN)/HOL  $(INTEG_FILES)
   6.126 +Integ:	$(BIN)/HOL  $(INTEG_FILES)
   6.127  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.128 -        then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
   6.129 -        else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
   6.130 -        fi
   6.131 +	then echo 'make_html := true; exit_use_dir"Integ";quit();' | $(LOGIC);\
   6.132 +	else echo 'exit_use_dir"Integ";quit();' | $(LOGIC); \
   6.133 +	fi
   6.134  
   6.135  ##I/O Automata
   6.136  IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
   6.137 -                Receiver Sender
   6.138 +		Receiver Sender
   6.139  IOA_ABP_NAMES = Action Correctness Lemmas
   6.140  IOA_MT_NAMES = Asig IOA Solve
   6.141  
   6.142 @@ -122,15 +122,15 @@
   6.143   $(IOA_ABP_NAMES:%=IOA/ABP/%.thy) $(IOA_ABP_NAMES:%=IOA/ABP/%.ML)\
   6.144   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
   6.145  
   6.146 -IOA:    $(BIN)/HOL  $(IOA_FILES)
   6.147 +IOA:	$(BIN)/HOL  $(IOA_FILES)
   6.148  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.149 -        then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
   6.150 -               | $(LOGIC);\
   6.151 -             echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
   6.152 -               | $(LOGIC);\
   6.153 -        else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
   6.154 +	then echo 'make_html := true; exit_use_dir"IOA/NTP";quit();' \
   6.155 +	       | $(LOGIC);\
   6.156 +	     echo 'make_html := true; exit_use_dir"IOA/ABP";quit();' \
   6.157 +	       | $(LOGIC);\
   6.158 +	else echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC); \
   6.159  	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
   6.160 -        fi
   6.161 +	fi
   6.162  
   6.163  
   6.164  ##Authentication & Security Protocols
   6.165 @@ -138,78 +138,78 @@
   6.166  
   6.167  AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
   6.168  
   6.169 -Auth:   $(BIN)/HOL  $(AUTH_FILES)
   6.170 +Auth:	$(BIN)/HOL  $(AUTH_FILES)
   6.171  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.172 -        then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
   6.173 -        else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
   6.174 -        fi
   6.175 +	then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
   6.176 +	else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
   6.177 +	fi
   6.178  
   6.179  
   6.180  ##Properties of substitutions
   6.181  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
   6.182  
   6.183  SUBST_FILES = Subst/ROOT.ML \
   6.184 -              $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   6.185 +	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
   6.186  
   6.187 -Subst:  $(BIN)/HOL  $(SUBST_FILES)
   6.188 +Subst:	$(BIN)/HOL  $(SUBST_FILES)
   6.189  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.190 -        then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
   6.191 -        else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
   6.192 -        fi
   6.193 +	then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
   6.194 +	else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
   6.195 +	fi
   6.196  
   6.197  ##Confluence of Lambda-calculus
   6.198  LAMBDA_NAMES = Lambda ParRed Commutation Eta
   6.199  
   6.200  LAMBDA_FILES = Lambda/ROOT.ML \
   6.201 -              $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   6.202 +	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
   6.203  
   6.204 -Lambda:  $(BIN)/HOL $(LAMBDA_FILES)
   6.205 +Lambda:	 $(BIN)/HOL $(LAMBDA_FILES)
   6.206  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.207 -        then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
   6.208 -               | $(LOGIC);\
   6.209 -        else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
   6.210 -        fi
   6.211 +	then echo 'make_html := true; exit_use_dir"Lambda";quit();' \
   6.212 +	       | $(LOGIC);\
   6.213 +	else echo 'exit_use_dir"Lambda";quit();' | $(LOGIC); \
   6.214 +	fi
   6.215  
   6.216  ##Type inference for MiniML
   6.217  MINIML_NAMES = I Maybe MiniML Type W
   6.218  
   6.219  MINIML_FILES = MiniML/ROOT.ML \
   6.220 -              $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   6.221 +	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
   6.222  
   6.223  MiniML: $(BIN)/HOL  $(MINIML_FILES)
   6.224  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.225 -        then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
   6.226 -               | $(LOGIC);\
   6.227 -        else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
   6.228 -        fi
   6.229 +	then echo 'make_html := true; exit_use_dir"MiniML";quit();' \
   6.230 +	       | $(LOGIC);\
   6.231 +	else echo 'exit_use_dir"MiniML";quit();' | $(LOGIC); \
   6.232 +	fi
   6.233  
   6.234  ##Lexical analysis
   6.235  LEX_FILES = Auto AutoChopper Chopper Prefix
   6.236  
   6.237  LEX_FILES = Lex/ROOT.ML \
   6.238 -            $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   6.239 +	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
   6.240  
   6.241  Lex:	$(BIN)/HOL  $(LEX_FILES)
   6.242  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.243 -        then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   6.244 -        else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   6.245 -        fi
   6.246 +	then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
   6.247 +	else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
   6.248 +	fi
   6.249  
   6.250  ##Miscellaneous examples
   6.251  EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
   6.252 -            Primes NatSum SList LList Acc PropLog Term Simult MT	    
   6.253 +	    Primes NatSum SList LList Acc PropLog Term Simult MT	    
   6.254  
   6.255  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
   6.256 -           ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   6.257 +	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
   6.258  
   6.259 -ex:     $(BIN)/HOL  $(EX_FILES)
   6.260 +ex:	$(BIN)/HOL  $(EX_FILES)
   6.261  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   6.262 -        then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
   6.263 -        else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   6.264 -        fi
   6.265 +	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
   6.266 +	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
   6.267 +	fi
   6.268  
   6.269  #Full test.
   6.270 -test:   $(BIN)/HOL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
   6.271 +test:	$(BIN)/HOL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
   6.272  	echo 'Test examples ran successfully' > test
   6.273  
   6.274  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL 
     7.1 --- a/src/HOLCF/Makefile	Mon Oct 14 11:08:54 1996 +0200
     7.2 +++ b/src/HOLCF/Makefile	Tue Oct 15 10:46:42 1996 +0200
     7.3 @@ -1,8 +1,8 @@
     7.4  # $Id$
     7.5  ############################################################################
     7.6 -#                                                                          #
     7.7 -#                   Makefile for Isabelle (HOLCF)                          #
     7.8 -#                                                                          #
     7.9 +#									   #
    7.10 +#		    Makefile for Isabelle (HOLCF)			   #
    7.11 +#									   #
    7.12  ############################################################################
    7.13  
    7.14  #To make the system, cd to this directory and type  
    7.15 @@ -33,52 +33,52 @@
    7.16  FILES = ROOT.ML Porder0.thy  $(THYS) $(THYS:.thy=.ML)
    7.17  
    7.18  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    7.19 -$(BIN)/HOLCF:   $(BIN)/HOL  $(FILES) 
    7.20 +$(BIN)/HOLCF:	$(BIN)/HOL  $(FILES) 
    7.21  	case "$(COMP)" in \
    7.22 -	poly*)  cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
    7.23 -                if [ "$${MAKE_HTML}" = "true" ]; \
    7.24 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    7.25 -                       | $(COMP) $(BIN)/HOLCF;\
    7.26 +	poly*)	cp $(BIN)/HOL $(BIN)/HOLCF; chmod u+w $(BIN)/HOLCF;\
    7.27 +		if [ "$${MAKE_HTML}" = "true" ]; \
    7.28 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    7.29 +		       | $(COMP) $(BIN)/HOLCF;\
    7.30  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.31 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/HOLCF;\
    7.32 -                else echo 'open PolyML; exit_use_dir".";' \
    7.33 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/HOLCF;\
    7.34 +		else echo 'open PolyML; exit_use_dir".";' \
    7.35  		       | $(COMP) $(BIN)/HOLCF;\
    7.36 -                fi;\
    7.37 +		fi;\
    7.38  		discgarb -c $(BIN)/HOLCF;;\
    7.39  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    7.40 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
    7.41 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    7.42 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/HOLCF" banner;' \
    7.43 -                       | $(BIN)/HOL;\
    7.44 -                else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
    7.45 -                       | $(BIN)/HOL;\
    7.46 -                fi;;\
    7.47 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/HOLCF" banner;' | $(BIN)/HOL;\
    7.48 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    7.49 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/HOLCF" banner;' \
    7.50 +		       | $(BIN)/HOL;\
    7.51 +		else echo 'exit_use_dir"."; xML"$(BIN)/HOLCF" banner;' \
    7.52 +		       | $(BIN)/HOL;\
    7.53 +		fi;;\
    7.54  	*)	echo Bad value for ISABELLECOMP: \
    7.55 -                	$(COMP) is not poly or sml;;\
    7.56 +			$(COMP) is not poly or sml;;\
    7.57  	esac
    7.58  
    7.59  $(BIN)/HOL:
    7.60  	cd ../HOL;  $(MAKE)
    7.61  
    7.62  EX_THYS =  ex/Fix2.thy ex/Hoare.thy \
    7.63 -           ex/Loop.thy  
    7.64 +	   ex/Loop.thy	
    7.65  
    7.66  EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    7.67  
    7.68 -test:   ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
    7.69 +test:	ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
    7.70  	case "$(COMP)" in \
    7.71  	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.72 -                then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    7.73 -                       | $(COMP) $(BIN)/HOLCF;\
    7.74 -                else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF;\
    7.75 -                fi;;\
    7.76 +		then echo 'make_html := true; exit_use_dir"ex"; quit();' \
    7.77 +		       | $(COMP) $(BIN)/HOLCF;\
    7.78 +		else echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF;\
    7.79 +		fi;;\
    7.80  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    7.81 -                then echo 'make_html := true; exit_use_dir"ex";' \
    7.82 -                       | $(BIN)/HOLCF;\
    7.83 -                else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
    7.84 -                fi;;\
    7.85 +		then echo 'make_html := true; exit_use_dir"ex";' \
    7.86 +		       | $(BIN)/HOLCF;\
    7.87 +		else echo 'exit_use_dir"ex";' | $(BIN)/HOLCF;\
    7.88 +		fi;;\
    7.89  	*)	echo Bad value for ISABELLECOMP: \
    7.90 -                	$(COMP) is not poly or sml;;\
    7.91 +			$(COMP) is not poly or sml;;\
    7.92  	esac
    7.93  
    7.94  EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
    7.95 @@ -89,21 +89,21 @@
    7.96  EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
    7.97  			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
    7.98  
    7.99 -test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF  $(EXPLICIT_DOMAINS_FILES) 
   7.100 +test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
   7.101  	case "$(COMP)" in \
   7.102  	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   7.103 -                then echo 'make_html := true; exit_use_dir"explicit_domains";                             quit();' | $(COMP) $(BIN)/HOLCF;\
   7.104 -                else echo 'exit_use_dir"explicit_domains"; quit();' \
   7.105 -                       | $(COMP) $(BIN)/HOLCF;\
   7.106 -                fi;;\
   7.107 +		then echo 'make_html := true; exit_use_dir"explicit_domains";				  quit();' | $(COMP) $(BIN)/HOLCF;\
   7.108 +		else echo 'exit_use_dir"explicit_domains"; quit();' \
   7.109 +		       | $(COMP) $(BIN)/HOLCF;\
   7.110 +		fi;;\
   7.111  	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   7.112 -                then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
   7.113 -                       | $(BIN)/HOLCF;\
   7.114 -                else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
   7.115 -                fi;;\
   7.116 +		then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
   7.117 +		       | $(BIN)/HOLCF;\
   7.118 +		else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
   7.119 +		fi;;\
   7.120  	*)	echo Bad value for ISABELLECOMP: \
   7.121 -                	$(COMP) is not poly or sml;;\
   7.122 +			$(COMP) is not poly or sml;;\
   7.123  	esac
   7.124  
   7.125 -.PRECIOUS:  $(BIN)/HOL  $(BIN)/HOLCF 
   7.126 +.PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF 
   7.127  
     8.1 --- a/src/LCF/Makefile	Mon Oct 14 11:08:54 1996 +0200
     8.2 +++ b/src/LCF/Makefile	Tue Oct 15 10:46:42 1996 +0200
     8.3 @@ -1,7 +1,7 @@
     8.4  # $Id$
     8.5  #########################################################################
     8.6  #									#
     8.7 -# 			Makefile for Isabelle (LCF)			#
     8.8 +#			Makefile for Isabelle (LCF)			#
     8.9  #									#
    8.10  #########################################################################
    8.11  
    8.12 @@ -21,42 +21,42 @@
    8.13  
    8.14  BIN = $(ISABELLEBIN)
    8.15  COMP = $(ISABELLECOMP)
    8.16 -FILES =  ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
    8.17 +FILES =	 ROOT.ML LCF.thy LCF.ML simpdata.ML pair.ML fix.ML
    8.18  
    8.19  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    8.20  $(BIN)/LCF:   $(BIN)/FOL  $(FILES) 
    8.21  	case "$(COMP)" in \
    8.22  	poly*)	cp $(BIN)/FOL $(BIN)/LCF;\
    8.23 -                if [ "$${MAKE_HTML}" = "true" ]; \
    8.24 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    8.25 -                       | $(COMP) $(BIN)/LCF;\
    8.26 +		if [ "$${MAKE_HTML}" = "true" ]; \
    8.27 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
    8.28 +		       | $(COMP) $(BIN)/LCF;\
    8.29  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    8.30 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/LCF;\
    8.31 -                else echo 'open PolyML; exit_use_dir".";' \
    8.32 -                       | $(COMP) $(BIN)/LCF;\
    8.33 -                fi;\
    8.34 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/LCF;\
    8.35 +		else echo 'open PolyML; exit_use_dir".";' \
    8.36 +		       | $(COMP) $(BIN)/LCF;\
    8.37 +		fi;\
    8.38  		discgarb -c $(BIN)/LCF;;\
    8.39  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
    8.40 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
    8.41 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    8.42 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/LCF" banner;' \
    8.43 -                       | $(BIN)/FOL;\
    8.44 -                else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
    8.45 -                       | $(BIN)/FOL;\
    8.46 -                fi;;\
    8.47 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/LCF" banner;' | $(BIN)/FOL;\
    8.48 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
    8.49 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/LCF" banner;' \
    8.50 +		       | $(BIN)/FOL;\
    8.51 +		else echo 'exit_use_dir"."; xML"$(BIN)/LCF" banner;' \
    8.52 +		       | $(BIN)/FOL;\
    8.53 +		fi;;\
    8.54  	*)	echo Bad value for ISABELLECOMP: \
    8.55 -                	$(COMP) is not poly or sml;;\
    8.56 +			$(COMP) is not poly or sml;;\
    8.57  	esac
    8.58  
    8.59  (BIN)/FOL:
    8.60  	cd ../FOL;  $(MAKE)
    8.61  
    8.62 -test:   ex.ML  $(BIN)/LCF
    8.63 +test:	ex.ML  $(BIN)/LCF
    8.64  	case "$(COMP)" in \
    8.65  	poly*)	echo 'exit_use"ex.ML"; quit();' | $(COMP) $(BIN)/LCF ;;\
    8.66  	sml*)	echo 'exit_use"ex.ML";' | $(BIN)/LCF;;\
    8.67  	*)	echo Bad value for ISABELLECOMP: \
    8.68 -                	$(COMP) is not poly or sml;;\
    8.69 +			$(COMP) is not poly or sml;;\
    8.70  	esac
    8.71  
    8.72 -.PRECIOUS:   $(BIN)/FOL  $(BIN)/LCF 
    8.73 +.PRECIOUS:   $(BIN)/FOL	 $(BIN)/LCF 
     9.1 --- a/src/Pure/Makefile	Mon Oct 14 11:08:54 1996 +0200
     9.2 +++ b/src/Pure/Makefile	Tue Oct 15 10:46:42 1996 +0200
     9.3 @@ -1,7 +1,7 @@
     9.4  #  $Id$
     9.5  #########################################################################
     9.6  #									#
     9.7 -# 			Makefile for Isabelle (Pure)			#
     9.8 +#			Makefile for Isabelle (Pure)			#
     9.9  #									#
    9.10  #########################################################################
    9.11  
    9.12 @@ -24,10 +24,10 @@
    9.13  FILES =	POLY.ML NJ.ML ROOT.ML library.ML term.ML symtab.ML type.ML sign.ML\
    9.14  	sequence.ML envir.ML pattern.ML unify.ML logic.ML theory.ML thm.ML\
    9.15  	net.ML display.ML deriv.ML drule.ML tctical.ML search.ML tactic.ML\
    9.16 -        goals.ML axclass.ML install_pp.ML\
    9.17 -        NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
    9.18 +	goals.ML axclass.ML install_pp.ML\
    9.19 +	NJ093.ML NJ1xx.ML ../Provers/simplifier.ML
    9.20  
    9.21 -SYNTAX_FILES =  Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
    9.22 +SYNTAX_FILES =	Syntax/ROOT.ML	Syntax/ast.ML		Syntax/lexicon.ML\
    9.23  	Syntax/parser.ML	Syntax/type_ext.ML	Syntax/syn_trans.ML\
    9.24  	Syntax/pretty.ML	Syntax/printer.ML	Syntax/syntax.ML\
    9.25  	Syntax/syn_ext.ML	Syntax/mixfix.ML
    9.26 @@ -36,25 +36,24 @@
    9.27  	Thy/thy_syn.ML		Thy/thy_read.ML		Thy/thm_database.ML
    9.28  
    9.29  #Uses cp rather than make_database because Poly/ML allows only 3 levels
    9.30 -$(BIN)/Pure:   $(FILES)  $(SYNTAX_FILES)  $(THY_FILES)  $(ML_DBASE)
    9.31 +$(BIN)/Pure:   $(FILES)	 $(SYNTAX_FILES)  $(THY_FILES)	$(ML_DBASE)
    9.32  	case "$(COMP)" in \
    9.33  	poly*)	echo database=$${ML_DBASE:?'No Poly/ML database specified'};\
    9.34  		cp $(ML_DBASE) $(BIN)/Pure; chmod u+w $(BIN)/Pure;\
    9.35  		echo 'PolyML.use"POLY";use"ROOT" handle _=> exit 1;' \
    9.36 -                  | $(COMP) $(BIN)/Pure;\
    9.37 +		  | $(COMP) $(BIN)/Pure;\
    9.38  		discgarb -c $(BIN)/Pure;;\
    9.39  	sml*)	if [ ! '(' -d $${ISABELLEBIN:?} -a -w $${ISABELLEBIN:?} ')' ];\
    9.40 -           	then echo Bad value for ISABELLEBIN: \
    9.41 -                	$(BIN) is not a writable directory; \
    9.42 -                	exit 1; \
    9.43 -           	fi;\
    9.44 -		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;                                    xML"$(BIN)/Pure" banner;' | $(COMP);;\
    9.45 +		then echo Bad value for ISABELLEBIN: \
    9.46 +			$(BIN) is not a writable directory; \
    9.47 +			exit 1; \
    9.48 +		fi;\
    9.49 +		echo 'use"NJ.ML"; use"ROOT.ML" handle _=> exit 1;				     xML"$(BIN)/Pure" banner;' | $(COMP);;\
    9.50  	*)	echo Bad value for ISABELLECOMP: \
    9.51 -                	$(COMP) is not poly or sml;;\
    9.52 +			$(COMP) is not poly or sml;;\
    9.53  	esac
    9.54  
    9.55  
    9.56  test: $(BIN)/Pure
    9.57 -	
    9.58  
    9.59 -.PRECIOUS:  $(BIN)/Pure  
    9.60 +.PRECIOUS:  $(BIN)/Pure	 
    10.1 --- a/src/Sequents/Makefile	Mon Oct 14 11:08:54 1996 +0200
    10.2 +++ b/src/Sequents/Makefile	Tue Oct 15 10:46:42 1996 +0200
    10.3 @@ -1,7 +1,7 @@
    10.4  # $Id$
    10.5  #########################################################################
    10.6  #									#
    10.7 -# 			Makefile for Isabelle (Sequents)		#
    10.8 +#			Makefile for Isabelle (Sequents)		#
    10.9  #									#
   10.10  #########################################################################
   10.11  
   10.12 @@ -31,39 +31,39 @@
   10.13      ex/ILL/ILL_kleene_lemmas.ML \
   10.14      $(ILL_NAMES:%=ex/ILL/%.thy) $(ILL_NAMES:%=ex/ILL/%.ML)
   10.15  
   10.16 -$(BIN)/Sequents:   $(BIN)/Pure  $(FILES) 
   10.17 +$(BIN)/Sequents:   $(BIN)/Pure	$(FILES) 
   10.18  	case "$(COMP)" in \
   10.19 -	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'  \
   10.20 +	poly*)	echo 'make_database"$(BIN)/Sequents"; quit();'	\
   10.21  			| $(COMP) $(BIN)/Pure;\
   10.22 -                if [ "$${MAKE_HTML}" = "true" ]; \
   10.23 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
   10.24 -                       | $(COMP) $(BIN)/Sequents;\
   10.25 +		if [ "$${MAKE_HTML}" = "true" ]; \
   10.26 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
   10.27 +		       | $(COMP) $(BIN)/Sequents;\
   10.28  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   10.29 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/Sequents;\
   10.30 -                else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/Sequents;\
   10.31 -                fi;\
   10.32 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/Sequents;\
   10.33 +		else echo 'open PolyML; exit_use_dir".";' | $(COMP) $(BIN)/Sequents;\
   10.34 +		fi;\
   10.35  		discgarb -c $(BIN)/Sequents;;\
   10.36  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
   10.37 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/Sequents" banner;' | $(BIN)/Pure;\
   10.38 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   10.39 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/Sequents" banner;' \
   10.40 -                       | $(BIN)/Pure;\
   10.41 -                else echo 'exit_use_dir"."; xML"$(BIN)/Sequents" banner;' \
   10.42 -                       | $(BIN)/Pure;\
   10.43 -                fi;;\
   10.44 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/Sequents" banner;' | $(BIN)/Pure;\
   10.45 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   10.46 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/Sequents" banner;' \
   10.47 +		       | $(BIN)/Pure;\
   10.48 +		else echo 'exit_use_dir"."; xML"$(BIN)/Sequents" banner;' \
   10.49 +		       | $(BIN)/Pure;\
   10.50 +		fi;;\
   10.51  	*)	echo Bad value for ISABELLECOMP: \
   10.52 -                	$(COMP) is not poly or sml;;\
   10.53 +			$(COMP) is not poly or sml;;\
   10.54  	esac
   10.55  
   10.56  $(BIN)/Pure:
   10.57  	cd ../Pure;  $(MAKE)
   10.58  
   10.59 -test:   $(BIN)/Sequents  $(EX_FILES)
   10.60 +test:	$(BIN)/Sequents	 $(EX_FILES)
   10.61  	case "$(COMP)" in \
   10.62  	poly*)	echo 'exit_use"ex/ROOT.ML";quit();' | $(COMP) $(BIN)/Sequents;;\
   10.63  	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/Sequents;;\
   10.64  	*)	echo Bad value for ISABELLECOMP: \
   10.65 -                	$(COMP) is not poly or sml;;\
   10.66 +			$(COMP) is not poly or sml;;\
   10.67  	esac
   10.68  
   10.69  
    11.1 --- a/src/ZF/Makefile	Mon Oct 14 11:08:54 1996 +0200
    11.2 +++ b/src/ZF/Makefile	Tue Oct 15 10:46:42 1996 +0200
    11.3 @@ -1,7 +1,7 @@
    11.4  # $Id$
    11.5  #########################################################################
    11.6  #									#
    11.7 -# 			Makefile for Isabelle (ZF)			#
    11.8 +#			Makefile for Isabelle (ZF)			#
    11.9  #									#
   11.10  #########################################################################
   11.11  
   11.12 @@ -31,31 +31,31 @@
   11.13  	Zorn Nat Finite List 
   11.14  
   11.15  FILES = ROOT.ML thy_syntax.ML ../Pure/section_utils.ML \
   11.16 - 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
   11.17 +	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
   11.18  
   11.19  #Uses cp rather than make_database because Poly/ML allows only 3 levels
   11.20 -$(BIN)/ZF:   $(BIN)/FOL  $(FILES) 
   11.21 +$(BIN)/ZF:   $(BIN)/FOL	 $(FILES) 
   11.22  	case "$(COMP)" in \
   11.23  	poly*)	cp $(BIN)/FOL $(BIN)/ZF;\
   11.24 -                if [ "$${MAKE_HTML}" = "true" ]; \
   11.25 -                then echo 'open PolyML; make_html := true; exit_use_dir".";' \
   11.26 -                       | $(COMP) $(BIN)/ZF;\
   11.27 +		if [ "$${MAKE_HTML}" = "true" ]; \
   11.28 +		then echo 'open PolyML; make_html := true; exit_use_dir".";' \
   11.29 +		       | $(COMP) $(BIN)/ZF;\
   11.30  		elif [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.31 -                then echo 'open PolyML; make_html := true; exit_use_dir".";                               make_html := false;' | $(COMP) $(BIN)/ZF;\
   11.32 -                else echo 'open PolyML; exit_use_dir".";' \
   11.33 -                       | $(COMP) $(BIN)/ZF;\
   11.34 -                fi;\
   11.35 +		then echo 'open PolyML; make_html := true; exit_use_dir".";				  make_html := false;' | $(COMP) $(BIN)/ZF;\
   11.36 +		else echo 'open PolyML; exit_use_dir".";' \
   11.37 +		       | $(COMP) $(BIN)/ZF;\
   11.38 +		fi;\
   11.39  		discgarb -c $(BIN)/ZF;;\
   11.40  	sml*)	if [ "$${MAKE_HTML}" = "true" ]; \
   11.41 -                then echo 'make_html := true; exit_use_dir".";                                            xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
   11.42 -                elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   11.43 -                then echo 'make_html := true; exit_use_dir".";                                            make_html := false; xML"$(BIN)/ZF" banner;' \
   11.44 -                       | $(BIN)/FOL;\
   11.45 -                else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
   11.46 -                       | $(BIN)/FOL;\
   11.47 -                fi;;\
   11.48 +		then echo 'make_html := true; exit_use_dir".";						  xML"$(BIN)/ZF" banner;' | $(BIN)/FOL;\
   11.49 +		elif [ "$${MAKE_HTML-undefined}" != "undefined" ];\
   11.50 +		then echo 'make_html := true; exit_use_dir".";						  make_html := false; xML"$(BIN)/ZF" banner;' \
   11.51 +		       | $(BIN)/FOL;\
   11.52 +		else echo 'exit_use_dir"."; xML"$(BIN)/ZF" banner;' \
   11.53 +		       | $(BIN)/FOL;\
   11.54 +		fi;;\
   11.55  	*)	echo Bad value for ISABELLECOMP: \
   11.56 -                	$(COMP) is not poly or sml; exit 1;;\
   11.57 +			$(COMP) is not poly or sml; exit 1;;\
   11.58  	esac
   11.59  
   11.60  $(BIN)/FOL:
   11.61 @@ -68,7 +68,7 @@
   11.62  	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/ZF" ;;\
   11.63  	sml*)	echo "$ISABELLEBIN/ZF" ;;\
   11.64  	*)	echo "echo Bad value for ISABELLECOMP: \
   11.65 -                	$ISABELLEBIN is not poly or sml; exit 1" ;;\
   11.66 +			$ISABELLEBIN is not poly or sml; exit 1" ;;\
   11.67  	esac
   11.68  
   11.69  ##IMP-semantics example
   11.70 @@ -77,68 +77,68 @@
   11.71  
   11.72  IMP:   $(BIN)/ZF  $(IMP_FILES)
   11.73  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.74 -        then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
   11.75 -        else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
   11.76 -        fi
   11.77 +	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
   11.78 +	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
   11.79 +	fi
   11.80  
   11.81  ##Coinduction example
   11.82  COIND_NAMES = ECR Language MT Map Static Types Values 
   11.83  
   11.84  COIND_FILES = Coind/ROOT.ML Coind/BCR.thy  Coind/Dynamic.thy \
   11.85 -              $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
   11.86 +	      $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
   11.87  
   11.88 -Coind:  $(BIN)/ZF  $(COIND_FILES)
   11.89 +Coind:	$(BIN)/ZF  $(COIND_FILES)
   11.90  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
   11.91 -        then echo 'make_html := true; exit_use_dir"Coind";quit();' | $(LOGIC);\
   11.92 -        else echo 'exit_use_dir"Coind";quit();' | $(LOGIC); \
   11.93 -        fi
   11.94 +	then echo 'make_html := true; exit_use_dir"Coind";quit();' | $(LOGIC);\
   11.95 +	else echo 'exit_use_dir"Coind";quit();' | $(LOGIC); \
   11.96 +	fi
   11.97  
   11.98  ##AC examples
   11.99  AC_NAMES = AC_Equiv OrdQuant Transrec2 Cardinal_aux \
  11.100  	   AC15_WO6 AC16_WO4 AC16_lemmas AC17_AC1 AC18_AC19 AC1_WO2 \
  11.101 -           DC DC_lemmas HH Hartog WO1_AC \
  11.102 -           WO2_AC16 WO6_WO1 WO_AC first recfunAC16 rel_is_fun
  11.103 +	   DC DC_lemmas HH Hartog WO1_AC \
  11.104 +	   WO2_AC16 WO6_WO1 WO_AC first recfunAC16 rel_is_fun
  11.105  
  11.106  AC_FILES = AC/ROOT.ML AC/AC0_AC1.ML AC/AC10_AC15.ML AC/AC1_AC17.ML \
  11.107 -           AC/AC2_AC6.ML AC/AC7_AC9.ML \
  11.108 -           AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
  11.109 -           $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
  11.110 +	   AC/AC2_AC6.ML AC/AC7_AC9.ML \
  11.111 +	   AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML \
  11.112 +	   $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
  11.113  
  11.114 -AC:  $(BIN)/ZF  $(AC_FILES)
  11.115 +AC:  $(BIN)/ZF	$(AC_FILES)
  11.116  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
  11.117 -        then echo 'make_html := true; exit_use_dir"AC";quit();' | $(LOGIC); \
  11.118 -        else echo 'exit_use_dir"AC";quit();' | $(LOGIC); \
  11.119 -        fi
  11.120 +	then echo 'make_html := true; exit_use_dir"AC";quit();' | $(LOGIC); \
  11.121 +	else echo 'exit_use_dir"AC";quit();' | $(LOGIC); \
  11.122 +	fi
  11.123  
  11.124  ##Residuals example
  11.125  
  11.126  RESID_NAMES = Confluence Redex SubUnion Conversion Reduction Substitution \
  11.127 -              Cube Residuals Terms
  11.128 +	      Cube Residuals Terms
  11.129  
  11.130  RESID_FILES = Resid/ROOT.ML $(RESID_NAMES:%=Resid/%.thy) \
  11.131 -                            $(RESID_NAMES:%=Resid/%.ML)
  11.132 +			    $(RESID_NAMES:%=Resid/%.ML)
  11.133  
  11.134 -Resid:  $(BIN)/ZF  $(RESID_FILES)
  11.135 +Resid:	$(BIN)/ZF  $(RESID_FILES)
  11.136  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
  11.137 -        then echo 'make_html := true; exit_use_dir"Resid";quit();' | $(LOGIC);\
  11.138 -        else echo 'exit_use_dir"Resid";quit();' | $(LOGIC); \
  11.139 -        fi
  11.140 +	then echo 'make_html := true; exit_use_dir"Resid";quit();' | $(LOGIC);\
  11.141 +	else echo 'exit_use_dir"Resid";quit();' | $(LOGIC); \
  11.142 +	fi
  11.143  
  11.144  ##Miscellaneous examples
  11.145  EX_NAMES = Primes Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
  11.146 -           Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit 
  11.147 +	   Data Enum Rmap Mutil PropLog ListN Acc Comb Primrec LList CoUnit 
  11.148  
  11.149  EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
  11.150  
  11.151  #Test ZF by loading the examples in directory ex
  11.152 -ex:     $(BIN)/ZF  $(EX_FILES)
  11.153 +ex:	$(BIN)/ZF  $(EX_FILES)
  11.154  	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
  11.155 -        then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC); \
  11.156 -        else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
  11.157 -        fi
  11.158 +	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC); \
  11.159 +	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
  11.160 +	fi
  11.161  
  11.162  #Full test.
  11.163 -test:   $(BIN)/ZF IMP Coind AC Resid ex
  11.164 +test:	$(BIN)/ZF IMP Coind AC Resid ex
  11.165  	echo 'Test examples ran successfully' > test
  11.166  
  11.167  .PRECIOUS:  $(BIN)/FOL $(BIN)/ZF