equal
deleted
inserted
replaced
3 Author: Tobias Nipkow, based on a theory by David von Oheimb |
3 Author: Tobias Nipkow, based on a theory by David von Oheimb |
4 Copyright 1997-2003 TU Muenchen |
4 Copyright 1997-2003 TU Muenchen |
5 |
5 |
6 The datatype of `maps' (written ~=>); strongly resembles maps in VDM. |
6 The datatype of `maps' (written ~=>); strongly resembles maps in VDM. |
7 *) |
7 *) |
|
8 |
|
9 header {* Maps *} |
8 |
10 |
9 theory Map = List: |
11 theory Map = List: |
10 |
12 |
11 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) |
13 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) |
12 |
14 |