diff -r e32b0eb63666 -r deb9b0283259 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Jan 09 14:07:39 2018 +0100
+++ b/src/HOL/Main.thy	Tue Jan 09 15:18:41 2018 +0100
@@ -17,11 +17,6 @@
     GCD
 begin
 
-text \<open>
-  Classical Higher-order Logic -- only ``Main'', excluding real and
-  complex numbers etc.
-\<close>
-
 no_notation
   bot ("\<bottom>") and
   top ("\<top>") and