| changeset 39757 | 21423597a80d |
| parent 35705 | 0e5251adb9cc |
| child 41413 | 64cd30d6b0b8 |
| 39755:93a10347e356 | 39757:21423597a80d |
|---|---|
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 |
1 |
8 no_document use_thys ["Nat_Bijection"]; |
2 no_document use_thys ["Nat_Bijection"]; |
9 use_thys ["Cardholder_Registration", "Merchant_Registration", "Purchase"]; |
3 use_thys ["SET_Protocol"]; |