--- 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