src/HOL/Library/Comparator.thy

--- a/src/HOL/Library/Comparator.thy	Fri Oct 26 14:12:08 2018 +0200
+++ b/src/HOL/Library/Comparator.thy	Fri Oct 26 08:20:45 2018 +0000
@@ -184,6 +184,8 @@
 
 end
 
+text \<open>Fundamental comparator combinators\<close>
+
 lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
   is "\<lambda>cmp a b. cmp b a"
 proof -