# HG changeset patch # User nipkow # Date 1525613351 -7200 # Node ID 7fe53815cce9a0d7f1bff442b29243797e412abe # Parent 152cc388cd1ee23f91cad2a4d18bdbaac467d961 reinstated old lemma name diff -r 152cc388cd1e -r 7fe53815cce9 src/HOL/List.thy --- a/src/HOL/List.thy Sun May 06 14:58:12 2018 +0200 +++ b/src/HOL/List.thy Sun May 06 15:29:11 2018 +0200 @@ -5625,6 +5625,8 @@ case False thus ?thesis by simp qed +lemmas sorted_list_of_set = set_sorted_list_of_set sorted_sorted_list_of_set distinct_sorted_list_of_set + lemma sorted_list_of_set_sort_remdups [code]: "sorted_list_of_set (set xs) = sort (remdups xs)" proof - @@ -6056,7 +6058,7 @@ lemma lexord_irrefl: "irrefl R \ irrefl (lexord R)" - by (simp add: irrefl_def lexord_irreflexive) +by (simp add: irrefl_def lexord_irreflexive) lemma lexord_asym: assumes "asym R"