Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comment makes no sense
authornipkow
Fri, 22 May 2020 19:21:16 +0200
changeset 71856 e9df7895e331
parent 71855 3e343c0c2138
child 71857 d73955442df5
child 71858 864fade05842
comment makes no sense
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle