removed dead code;

--- a/src/HOL/Cardinals/document/root.tex	Mon Oct 20 10:19:50 2014 +0200
+++ b/src/HOL/Cardinals/document/root.tex	Mon Oct 20 14:11:14 2014 +0200
@@ -8,10 +8,8 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
+\bibliographystyle{plain}
 
-\bibliographystyle{plain}
 \begin{document}
 
 \title{Ordinals and cardinals in HOL}