changeset 71856 | e9df7895e331 |
parent 71855 | 3e343c0c2138 |
child 71857 | d73955442df5 |
--- 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