| changeset 25595 | 6c48275f9c76 |
| parent 24423 | ae9cd0e92423 |
| child 25885 | 6fbc3f54f819 |
| 25594:43c718438f9f | 25595:6c48275f9c76 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Implementation of finite sets by lists *} |
6 header {* Implementation of finite sets by lists *} |
7 |
7 |
8 theory Executable_Set |
8 theory Executable_Set |
9 imports Main |
9 imports List |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Definitional rewrites *} |
12 subsection {* Definitional rewrites *} |
13 |
13 |
14 lemma [code target: Set]: |
14 lemma [code target: Set]: |