equal
deleted
inserted
replaced
1 (****************************************************************************** |
1 (* Title: HOL/Auth/Guard/List_Msg.thy |
2 date: november 2001 |
2 Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
3 author: Frederic Blanqui |
3 Copyright 2001 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{*Lists of Messages and Lists of Agents*} |
6 header{*Lists of Messages and Lists of Agents*} |
13 |
7 |
14 theory List_Msg imports Extensions begin |
8 theory List_Msg imports Extensions begin |
15 |
9 |