src/HOL/SET_Protocol/ROOT.ML
changeset 33028 9aa8bfb1649d
parent 29909 9433df099848
child 33615 261abc2e3155
equal deleted inserted replaced
33027:9cf389429f6d 33028:9aa8bfb1649d
       
     1 (*  Title:      HOL/SET_Protocol/ROOT.ML
       
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
       
     3     Copyright   2003  University of Cambridge
       
     4 
       
     5 Root file for the SET protocol proofs.
       
     6 *)
       
     7 
       
     8 no_document use_thy "Nat_Int_Bij";
       
     9 use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];