| changeset 30738 | 0842e906300c |
| parent 28041 | f496e9f343b7 |
| child 37075 | a680ce27aa56 |
| 30737:9ffd27558916 | 30738:0842e906300c |
|---|---|
1 (* ID: $Id$ |
1 (* Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
|
3 Copyright 1994 TU Muenchen |
2 Copyright 1994 TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header{*Quicksort*} |
5 header{*Quicksort*} |
7 |
6 |
8 theory Quicksort |
7 theory Quicksort |
9 imports Plain Multiset |
8 imports Main Multiset |
10 begin |
9 begin |
11 |
10 |
12 context linorder |
11 context linorder |
13 begin |
12 begin |
14 |
13 |