--- a/src/HOL/Real/HahnBanach/document/bbb.sty Sat Dec 16 21:41:14 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-%
-% home made blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
-%
-
-\def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
-\def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
-\def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
-\def\bbbE{{{\rm I}\mkern-3.8mu{\rm E}}}
-\def\bbbF{{{\rm I}\mkern-3.8mu{\rm F}}}
-\def\bbbG{{{\rm G}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbH{{{\rm I}\mkern-3.8mu{\rm H}}}
-\def\bbbI{{{\rm I}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
-\def\bbbJ{{{\rm J}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
-\def\bbbK{{{\rm I}\mkern-3.8mu{\rm K}}}
-\def\bbbL{{{\rm I}\mkern-3.8mu{\rm L}}}
-\def\bbbM{{{\rm I}\mkern-3.8mu{\rm M}}}
-\def\bbbN{{{\rm I}\mkern-3.8mu{\rm N}}}
-\def\bbbO{{{\rm O}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbP{{{\rm I}\mkern-3.8mu{\rm P}}}
-\def\bbbQ{{{\rm Q}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbR{{{\rm I}\mkern-3.8mu{\rm R}}}
-\def\bbbT{{{\rm T}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
-\def\bbbU{{{\rm U}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
-\def\bbbZ{{{\sf Z}\mkern-7.5mu{\sf Z}}}