src/HOLCF/Makefile

 # $Id$
 ############################################################################
-#                                                                          #
-#                   Makefile for Isabelle (HOLCF)                          #
-#                                                                          #
+#									   #
+#		    Makefile for Isabelle (HOLCF)			   #
+#									   #
 ############################################################################
 
 #To make the system, cd to this directory and type  
 #	make
 #To make the system and test it on standard examples, type 

        Tr1.thy Tr2.thy HOLCF.thy 
 
 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 \
 			explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
 			explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy\
 			explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
 
 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