src/HOL/Real/HahnBanach/document/bbb.sty

Goal: tuned pris;

%
% 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}}}