diff -r 9cf389429f6d -r 9aa8bfb1649d src/HOL/SET_Protocol/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SET_Protocol/ROOT.ML Tue Oct 20 20:03:23 2009 +0200 @@ -0,0 +1,9 @@ +(* 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_thy "Nat_Int_Bij"; +use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];