isabelle: src/HOL/SET_Protocol/SET_Protocol.thy@316d94b4ffe2 (annotated)

39769 5bcf4253d579 modernized session haftmann parents: diff changeset	1	(* Title: HOL/SET_Protocol/SET_Protocol.thy
5bcf4253d579 modernized session haftmann parents: diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5bcf4253d579 modernized session haftmann parents: diff changeset	3	Copyright 2003 University of Cambridge
5bcf4253d579 modernized session haftmann parents: diff changeset	4
5bcf4253d579 modernized session haftmann parents: diff changeset	5	Root file for the SET protocol proofs.
5bcf4253d579 modernized session haftmann parents: diff changeset	6	*)
5bcf4253d579 modernized session haftmann parents: diff changeset	7
5bcf4253d579 modernized session haftmann parents: diff changeset	8	theory SET_Protocol
5bcf4253d579 modernized session haftmann parents: diff changeset	9	imports Cardholder_Registration Merchant_Registration Purchase
5bcf4253d579 modernized session haftmann parents: diff changeset	10	begin
5bcf4253d579 modernized session haftmann parents: diff changeset	11
5bcf4253d579 modernized session haftmann parents: diff changeset	12	end