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