src/HOL/Makefile

 	../Provers/hypsubst.ML ../Provers/classical.ML\
 	../Provers/simplifier.ML ../Provers/splitter.ML\
 	$(NAMES:%=%.thy) $(NAMES:%=%.ML)
 
 $(BIN)/HOL:   $(BIN)/Pure  $(FILES) 
-	if [ -d $${ISABELLEBIN:?}/Pure ];\
+	@if [ -d $${ISABELLEBIN:?}/Pure ];\
 		then echo Bad value for ISABELLEBIN: \
 			$(BIN) is the Isabelle source directory; \
 			exit 1; \
-		fi;\
-	case "$(COMP)" in \
+	fi
+	@case `expr "//$(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;\

 		       | $(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:
 	cd ../Pure;  $(MAKE)
 
 #### Testing of HOL
 
 #A macro referring to the object-logic (depends on ML compiler)
-LOGIC:sh=case $ISABELLECOMP in \
+LOGIC:sh=case `expr "//$ISABELLECOMP" : '[^ ]*/\(.*\)'` in \
 	poly*)	echo "$ISABELLECOMP $ISABELLEBIN/HOL" ;;\
 	sml*)	echo "$ISABELLEBIN/HOL" ;;\
-	*)	echo "echo Bad value for ISABELLECOMP: \
-			$ISABELLEBIN is not poly or sml; exit 1" ;;\
+	*)	echo "echo; echo Bad value for ISABELLECOMP: \
+			$ISABELLECOMP 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)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"IMP";quit();' | $(LOGIC); \
 	else echo 'exit_use_dir"IMP";quit();' | $(LOGIC); \
 	fi
 
 ##Hoare logic
 Hoare_NAMES = Hoare Arith2 Examples
 Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) \
 	      $(Hoare_NAMES:%=Hoare/%.ML)
 
 Hoare:	$(BIN)/HOL  $(Hoare_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Hoare";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Hoare";quit();' | $(LOGIC); \
 	fi
 
 ##The integers in HOL

 
 INTEG_FILES = Integ/ROOT.ML \
 	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
 
 Integ:	$(BIN)/HOL  $(INTEG_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@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
 
 ##I/O Automata

  IOA/ABP/Receiver.thy IOA/ABP/Sender.thy IOA/ABP/Spec.thy\
  $(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)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@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); \
 	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
 	fi
 
 
 ##Authentication & Security Protocols
-Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN Yahalom
+Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \
+	     Yahalom Yahalom2
 
 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
 
 Auth:	$(BIN)/HOL  $(AUTH_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@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
 
 

 
 SUBST_FILES = Subst/ROOT.ML \
 	      $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
 
 Subst:	$(BIN)/HOL  $(SUBST_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Subst";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Subst";quit();' | $(LOGIC); \
 	fi
 
 ##Confluence of Lambda-calculus

 
 LAMBDA_FILES = Lambda/ROOT.ML \
 	      $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
 
 Lambda:	 $(BIN)/HOL $(LAMBDA_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@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
 

 
 MINIML_FILES = MiniML/ROOT.ML \
 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
 
 MiniML: $(BIN)/HOL  $(MINIML_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@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
 

 
 LEX_FILES = Lex/ROOT.ML \
 	    $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
 
 Lex:	$(BIN)/HOL  $(LEX_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"Lex";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"Lex";quit();' | $(LOGIC); \
 	fi
 
 ##Miscellaneous examples

 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
 	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
 
 ex:	$(BIN)/HOL  $(EX_FILES)
-	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
 	then echo 'make_html := true; exit_use_dir"ex";quit();' | $(LOGIC);\
 	else echo 'exit_use_dir"ex";quit();' | $(LOGIC); \
 	fi
 
 #Full test.