src/HOL/Library/List_Lexorder.thy
changeset 78789 f2e845c3e65c
parent 72184 881bd98bddee