# HG changeset patch
# User nipkow
# Date 1590168076 -7200
# Node ID e9df7895e3310bec8a39c0e287d4aea9c357b0c3
# Parent  3e343c0c2138156813352e5874264f318d6f03c2
comment makes no sense

diff -r 3e343c0c2138 -r e9df7895e331 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 22 08:52:23 2020 +0200
+++ b/src/HOL/List.thy	Fri May 22 19:21:16 2020 +0200
@@ -365,8 +365,6 @@
 "sorted_wrt P [] = True" |
 "sorted_wrt P (x # ys) = ((\<forall>y \<in> set ys. P x y) \<and> sorted_wrt P ys)"
 
-(* FIXME: define sorted in terms of sorted_wrt *)
-
 text \<open>A class-based sorted predicate:\<close>
 
 context linorder