diff -r 7fedc55c14d5 -r d328d0d9b88e doc/manual/en/html/manual.css
--- a/doc/manual/en/html/manual.css	Thu Aug 02 14:20:52 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-/* Century Schoolbook font is very similar to Computer Modern Math: cmmi */
-.MATH    { font-family: "Century Schoolbook", serif; }
-.MATH I  { font-family: "Century Schoolbook", serif; font-style: italic }
-.BOLDMATH { font-family: "Century Schoolbook", serif; font-weight: bold }
-
-/* implement both fixed-size and relative sizes */
-SMALL.XTINY		{ font-size : xx-small }
-SMALL.TINY		{ font-size : x-small  }
-SMALL.SCRIPTSIZE	{ font-size : smaller  }
-SMALL.FOOTNOTESIZE	{ font-size : small    }
-SMALL.SMALL		{  }
-BIG.LARGE		{  }
-BIG.XLARGE		{ font-size : large    }
-BIG.XXLARGE		{ font-size : x-large  }
-BIG.HUGE		{ font-size : larger   }
-BIG.XHUGE		{ font-size : xx-large }
-
-/* heading styles */
-H1		{  }
-H2		{  }
-H3		{  }
-H4		{  }
-H5		{  }
-
-/* mathematics styles */
-DIV.displaymath		{ }	/* math displays */
-TD.eqno			{ }	/* equation-number cells */
-
-
-/* document-specific styles come next */
-DIV.navigation		{   }
-SPAN.bfseries		{   }
-DIV.center		{   }
-SPAN.upshape		{   }
-SPAN.mdseries		{   }
-SPAN.alph		{   }
-SPAN.arabic		{   }
-SPAN.textbf		{ font-weight: bold  }
-SPAN.roman		{   }
-#hue725		{ color: #000000;  }