# HG changeset patch
# User wenzelm
# Date 1515507521 -3600
# Node ID deb9b028325926dbc05f7e375708a50974b59564
# Parent  e32b0eb63666f4cddd1e6685ca180f192f1953a6
removed duplicate text;

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