--- a/src/HOL/Main.thy Sat Apr 09 11:35:01 2016 +0200
+++ b/src/HOL/Main.thy Sat Apr 09 12:36:25 2016 +0200
@@ -9,8 +9,6 @@
complex numbers etc.
\<close>
-text \<open>See further @{cite "Nipkow-et-al:2002:tutorial"}\<close>
-
no_notation
bot ("\<bottom>") and
top ("\<top>") and