| author | Fabian Huch <huch@in.tum.de> | 
| Fri, 01 Dec 2023 20:32:34 +0100 | |
| changeset 79101 | 4e47b34fbb8e | 
| parent 39769 | 5bcf4253d579 | 
| permissions | -rw-r--r-- | 
| 39769 | 1 | (* Title: HOL/SET_Protocol/SET_Protocol.thy | 
| 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 | theory SET_Protocol | |
| 9 | imports Cardholder_Registration Merchant_Registration Purchase | |
| 10 | begin | |
| 11 | ||
| 12 | end |