equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Map operations implemented on association lists*} |
6 header {* Map operations implemented on association lists*} |
7 |
7 |
8 theory AssocList |
8 theory AssocList |
9 imports Plain Map |
9 imports Plain "~~/src/HOL/Map" |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 The operations preserve distinctness of keys and |
13 The operations preserve distinctness of keys and |
14 function @{term "clearjunk"} distributes over them. Since |
14 function @{term "clearjunk"} distributes over them. Since |