# HG changeset patch # User haftmann # Date 1285680670 -7200 # Node ID 5bcf4253d57943fc8053ef6abef412b4205f0561 # Parent 1c46d4f8afd2b978da1ed63777623ed73763a6c0 modernized session diff -r 1c46d4f8afd2 -r 5bcf4253d579 src/HOL/SET_Protocol/SET_Protocol.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SET_Protocol/SET_Protocol.thy Tue Sep 28 15:31:10 2010 +0200 @@ -0,0 +1,12 @@ +(* Title: HOL/SET_Protocol/SET_Protocol.thy + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2003 University of Cambridge + +Root file for the SET protocol proofs. +*) + +theory SET_Protocol +imports Cardholder_Registration Merchant_Registration Purchase +begin + +end