diff -r a5853334c179 -r 499a63c30d55 src/HOL/Main.thy --- 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. \ -text \See further @{cite "Nipkow-et-al:2002:tutorial"}\ - no_notation bot ("\") and top ("\") and