# 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 \<Longrightarrow> irrefl (lexord R)"
-  by (simp add: irrefl_def lexord_irreflexive)
+by (simp add: irrefl_def lexord_irreflexive)
 
 lemma lexord_asym:
   assumes "asym R"