# HG changeset patch
# User wenzelm
# Date 1413807074 -7200
# Node ID cb8d2470623b8a47be848e4019a66f9379f8461f
# Parent  ca0b7d7cc9a37fa8ada937b18049f3e36389dce0
removed dead code;

diff -r ca0b7d7cc9a3 -r cb8d2470623b src/HOL/Cardinals/document/root.tex
--- 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}