--- a/src/HOL/IsaMakefile Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 28 12:47:55 2010 +0200
@@ -1053,7 +1053,7 @@
SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \
SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \
SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \
- SET_Protocol/document/root.tex
+ SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
--- a/src/HOL/SET_Protocol/ROOT.ML Tue Sep 28 12:10:37 2010 +0200
+++ b/src/HOL/SET_Protocol/ROOT.ML Tue Sep 28 12:47:55 2010 +0200
@@ -1,9 +1,3 @@
-(* Title: HOL/SET_Protocol/ROOT.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2003 University of Cambridge
-
-Root file for the SET protocol proofs.
-*)
no_document use_thys ["Nat_Bijection"];
-use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];
+use_thys ["SET_Protocol"];