equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow, Peter Lammich *) |
1 (* Author: Tobias Nipkow, Peter Lammich *) |
2 |
2 |
3 section \<open>Priority Queue Interface\<close> |
3 section \<open>Priority Queue Interface\<close> |
4 |
4 |
5 theory Priority_Queue |
5 theory Priority_Queue |
6 imports "~~/src/HOL/Library/Multiset" |
6 imports "HOL-Library.Multiset" |
7 begin |
7 begin |
8 |
8 |
9 text \<open>Priority queue interface:\<close> |
9 text \<open>Priority queue interface:\<close> |
10 |
10 |
11 locale Priority_Queue = |
11 locale Priority_Queue = |