changeset 58623 | 2db1df2c8467 |
parent 58377 | c6f93b8d2d8e |
child 58770 | ae5e9b4f8daf |
--- a/src/HOL/Main.thy Tue Oct 07 23:12:08 2014 +0200 +++ b/src/HOL/Main.thy Tue Oct 07 23:29:43 2014 +0200 @@ -10,7 +10,7 @@ complex numbers etc. *} -text {* See further \cite{Nipkow-et-al:2002:tutorial} *} +text {* See further @{cite "Nipkow-et-al:2002:tutorial"} *} no_notation bot ("\<bottom>") and