src/HOL/SET_Protocol/ROOT.ML
changeset 39757 21423597a80d
parent 35705 0e5251adb9cc
child 41413 64cd30d6b0b8
--- 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"];