comment makes no sense
authornipkow
Fri May 22 19:21:16 2020 +0200 (7 weeks ago)
changeset 71856e9df7895e331
parent 71855 3e343c0c2138
child 71857 d73955442df5
child 71858 864fade05842
comment makes no sense
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri May 22 08:52:23 2020 +0200
     1.2 +++ b/src/HOL/List.thy	Fri May 22 19:21:16 2020 +0200
     1.3 @@ -365,8 +365,6 @@
     1.4  "sorted_wrt P [] = True" |
     1.5  "sorted_wrt P (x # ys) = ((\<forall>y \<in> set ys. P x y) \<and> sorted_wrt P ys)"
     1.6  
     1.7 -(* FIXME: define sorted in terms of sorted_wrt *)
     1.8 -
     1.9  text \<open>A class-based sorted predicate:\<close>
    1.10  
    1.11  context linorder