src/HOL/Makefile
changeset 1972 cc65911dceef
parent 1862 74d4ae2f6fc3
child 1981 432db3edccdc
     1.1 --- a/src/HOL/Makefile	Tue Sep 10 11:35:23 1996 +0200
     1.2 +++ b/src/HOL/Makefile	Tue Sep 10 11:37:52 1996 +0200
     1.3 @@ -131,6 +131,19 @@
     1.4  	     echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC); \
     1.5          fi
     1.6  
     1.7 +
     1.8 +##Authentication & Security Protocols
     1.9 +Auth_NAMES = Message Shared NS_Shared OtwayRees
    1.10 +
    1.11 +AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML)
    1.12 +
    1.13 +Auth:   $(BIN)/HOL  $(AUTH_FILES)
    1.14 +	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    1.15 +        then echo 'make_html := true; exit_use_dir"Auth";quit();' | $(LOGIC);\
    1.16 +        else echo 'exit_use_dir"Auth";quit();' | $(LOGIC); \
    1.17 +        fi
    1.18 +
    1.19 +
    1.20  ##Properties of substitutions
    1.21  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
    1.22  
    1.23 @@ -195,7 +208,7 @@
    1.24          fi
    1.25  
    1.26  #Full test.
    1.27 -test:   $(BIN)/HOL IMP Hoare Lex Integ Subst Lambda MiniML IOA ex
    1.28 +test:   $(BIN)/HOL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
    1.29  	echo 'Test examples ran successfully' > test
    1.30  
    1.31  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL