src/HOL/IsaMakefile

   HOL-MiniML \
   HOL-Modelcheck \
   HOL-NanoJava \
   HOL-NumberTheory \
   HOL-Prolog \
+  HOL-SET-Protocol \
   HOL-Subst \
       TLA-Buffer \
       TLA-Inc \
       TLA-Memory \
   HOL-UNITY \

   UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy\
   UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy\
   UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
   UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
   UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \
-  UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy  \
-  UNITY/Simple/Network.thy\
+  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\
   UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
   UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
   UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
   UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
   UNITY/Comp/PriorityAux.thy \

   Isar_examples/document/root.bib Isar_examples/document/root.tex \
   Isar_examples/document/style.tex Hoare/hoare.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
 
 
+## HOL-SET-Protocol
+
+HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz
+
+$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \
+  SET-Protocol/MessageSET.thy\
+  SET-Protocol/EventSET.thy\
+  SET-Protocol/PublicSET.thy\
+  SET-Protocol/Cardholder_Registration.thy\
+  SET-Protocol/Merchant_Registration.thy\
+  SET-Protocol/Purchase.thy\
+  SET-Protocol/document/root.tex 
+	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
+
+
+
 ## TLA
 
 TLA: HOL $(OUT)/TLA
 
 $(OUT)/TLA: $(OUT)/HOL TLA/Action.ML TLA/Action.thy TLA/Init.ML \

 		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice \
 		$(LOG)/HOL-Complex.gz \
 		$(LOG)/HOL-Complex-ex.gz \
-		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/TLA-Inc.gz \
-		$(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
+		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
+                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
 		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz