src/HOL/Data_Structures/Sorting.thy
Tue, 11 Sep 2018 22:25:00 +0200 nipkow tuned proof
Tue, 11 Sep 2018 18:12:11 +0200 nipkow simplified defns
Tue, 11 Sep 2018 17:53:08 +0200 nipkow "undefined" not needed, [] is perfectly natural
less more (0) -10 -3 tip