src/HOL/SET-Protocol/ROOT.ML
author chaieb
Mon, 09 Feb 2009 11:07:17 +0000
changeset 29835 62da280e5d0b
parent 28098 c92850d2d16c
child 29909 9433df099848
permissions -rw-r--r--
A formalization of finite cartesian product types

(*  Title:      HOL/SET-Protocol/ROOT.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   2003  University of Cambridge

Root file for the SET protocol proofs.
*)

use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"];