equal
deleted
inserted
replaced
1 (****************************************************************************** |
1 (* Title: HOL/Auth/Guard/Guard_OtwayRees.thy |
2 date: march 2002 |
2 Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
3 author: Frederic Blanqui |
3 Copyright 2002 University of Cambridge |
4 email: blanqui@lri.fr |
4 *) |
5 webpage: http://www.lri.fr/~blanqui/ |
|
6 |
|
7 University of Cambridge, Computer Laboratory |
|
8 William Gates Building, JJ Thomson Avenue |
|
9 Cambridge CB3 0FD, United Kingdom |
|
10 ******************************************************************************) |
|
11 |
5 |
12 header{*Otway-Rees Protocol*} |
6 header{*Otway-Rees Protocol*} |
13 |
7 |
14 theory Guard_OtwayRees imports Guard_Shared begin |
8 theory Guard_OtwayRees imports Guard_Shared begin |
15 |
9 |