isabelle: src/HOL/ex/Qsort.thy@f990040535c9 (annotated)

8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	1	(* Title: HOL/ex/Qsort.thy
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1376 diff changeset	3	Author: Tobias Nipkow
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	4	Copyright 1994 TU Muenchen
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	5
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	6	Quicksort
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	7	*)
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	8
b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	9	Qsort = Sorting +
8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	10	consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	11
8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	12	recdef qsort "measure (size o snd)"
8524 f990040535c9 a possibly (?) more perspicous simprule in the "simpset" part paulson parents: 8414 diff changeset	13	simpset "simpset() addsimps [length_filter RS le_less_trans]"
8414 5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	14
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	15	"qsort(le, []) = []"
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	16
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	17	"qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	18	@ (x # qsort(le, [y:xs . le x y]))"
5983668cac15 now uses recdef instead of "rules" paulson parents: 1476 diff changeset	19
969 b051e2fc2e34 converted ex with curried function application clasohm parents: diff changeset	20	end

author	paulson
	Mon, 20 Mar 2000 10:26:34 +0100
changeset 8524	f990040535c9
parent 8414	5983668cac15
child 8590	89675b444abe
permissions	-rw-r--r--