# 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 \ - Classical Higher-order Logic -- only ``Main'', excluding real and - complex numbers etc. -\ - no_notation bot ("\") and top ("\") and