src/HOL/Library/List_Lenlexorder.thy
Tue, 02 Aug 2022 12:19:05 +0100 paulson The wellordering instantiation for length-ordered lists
Fri, 21 Aug 2020 12:42:57 +0100 paulson reversing all the lex crap
Mon, 17 Aug 2020 15:42:38 +0100 paulson S Holub's proposed generalisation of the lexicographic product of two orderings
Fri, 17 Apr 2020 20:55:53 +0100 paulson New theory Library/List_Lenlexorder.thy, a type class instantiation for well-ordering lists
less more (0) tip