equal
deleted
inserted
replaced
1 (* Title: HOL/Auth/Guard/Guard_Shared.thy |
1 (* Title: HOL/Auth/Guard/Guard_Shared.thy |
2 Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
2 Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
3 Copyright 2002 University of Cambridge |
3 Copyright 2002 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 header{*lemmas on guarded messages for protocols with symmetric keys*} |
6 section{*lemmas on guarded messages for protocols with symmetric keys*} |
7 |
7 |
8 theory Guard_Shared imports Guard GuardK "../Shared" begin |
8 theory Guard_Shared imports Guard GuardK "../Shared" begin |
9 |
9 |
10 subsection{*Extensions to Theory @{text Shared}*} |
10 subsection{*Extensions to Theory @{text Shared}*} |
11 |
11 |