equal
deleted
inserted
replaced
1 /* Title: Pure/General/multi_map.scala |
1 /* Title: Pure/General/multi_map.scala |
2 Module: PIDE |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 Maps with multiple entries per key. |
4 Maps with multiple entries per key. |
6 */ |
5 */ |
7 |
6 |