| changeset 42637 | 381fdcab0f36 |
| parent 39795 | 9e59b4c11039 |
| child 46471 | 2289a3869c88 |
| 42636:41dff1b862bf | 42637:381fdcab0f36 |
|---|---|
1 (* Title: HOL/Auth/Event |
1 (* Title: HOL/Auth/Event |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1996 University of Cambridge |
3 Copyright 1996 University of Cambridge |
5 |
4 |
6 Datatype of events; function "spies"; freshness |
5 Datatype of events; function "spies"; freshness |
7 |
6 |