author | paulson |
Mon, 20 Mar 2000 10:26:34 +0100 | |
changeset 8524 | f990040535c9 |
parent 8414 | 5983668cac15 |
child 8590 | 89675b444abe |
permissions | -rw-r--r-- |
(* Title: HOL/ex/Qsort.thy ID: $Id$ Author: Tobias Nipkow Copyright 1994 TU Muenchen Quicksort *) Qsort = Sorting + consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list" recdef qsort "measure (size o snd)" simpset "simpset() addsimps [length_filter RS le_less_trans]" "qsort(le, []) = []" "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y]) @ (x # qsort(le, [y:xs . le x y]))" end