equal
deleted
inserted
replaced
134 fi |
134 fi |
135 |
135 |
136 |
136 |
137 ##Authentication & Security Protocols |
137 ##Authentication & Security Protocols |
138 Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \ |
138 Auth_NAMES = Message Shared NS_Shared OtwayRees OtwayRees_AN OtwayRees_Bad \ |
139 WooLam Yahalom Yahalom2 |
139 WooLam Yahalom Yahalom2 Public NS_Public_Bad NS_Public |
140 |
140 |
141 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) |
141 AUTH_FILES = Auth/ROOT.ML $(AUTH_NAMES:%=Auth/%.thy) $(AUTH_NAMES:%=Auth/%.ML) |
142 |
142 |
143 Auth: $(BIN)/HOL $(AUTH_FILES) |
143 Auth: $(BIN)/HOL $(AUTH_FILES) |
144 @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |
144 @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \ |