# HG changeset patch
# User haftmann
# Date 1285670875 -7200
# Node ID 21423597a80da2c0e43a44ad1ce20243d7eaac99
# Parent  93a10347e356fae67bc844955703bc38208594eb
modernized session

diff -r 93a10347e356 -r 21423597a80d src/HOL/IsaMakefile
--- 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
 
 
diff -r 93a10347e356 -r 21423597a80d src/HOL/SET_Protocol/ROOT.ML
--- 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"];