src/HOL/List.thy

   case True thus ?thesis by(induction A) (simp_all add: distinct_insort)
 next
   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 -
   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   show ?thesis by (simp add: sorted_list_of_set.eq_fold sort_conv_fold fold_set_fold_remdups)

   apply (rule allI, case_tac x, simp, simp)
   by blast
 
 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"
   shows "asym (lexord R)"
 proof