| changeset 61343 | 5b5656a63bd6 |
| parent 60515 | 484559628038 |
| child 66453 | cc19f7ca2ed6 |
| 61342:b98cd131e2b5 | 61343:5b5656a63bd6 |
|---|---|
1 (* Title: HOL/ex/MergeSort.thy |
1 (* Title: HOL/ex/MergeSort.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 2002 TU Muenchen |
3 Copyright 2002 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 section{*Merge Sort*} |
6 section\<open>Merge Sort\<close> |
7 |
7 |
8 theory MergeSort |
8 theory MergeSort |
9 imports "~~/src/HOL/Library/Multiset" |
9 imports "~~/src/HOL/Library/Multiset" |
10 begin |
10 begin |
11 |
11 |