| changeset 47 | 69d815b0e1eb |
| parent 46 | a73f8a7784bd |
| child 48 | 21291189b51e |
| 46:a73f8a7784bd | 47:69d815b0e1eb |
|---|---|
1 (* Title: HOL/ex/sorting.thy |
1 (* Title: HOL/ex/sorting.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 Specifikation of sorting |
6 Specification of sorting |
7 *) |
7 *) |
8 |
8 |
9 Sorting = List + |
9 Sorting = List + |
10 consts |
10 consts |
11 sorted1:: "[['a,'a] => bool, 'a list] => bool" |
11 sorted1:: "[['a,'a] => bool, 'a list] => bool" |