src/HOL/Real/HahnBanach/document/bbb.sty
changeset 7984 86c0cc789f61
parent 7978 1b99ee57d131
equal deleted inserted replaced
7983:d823fdcc0645 7984:86c0cc789f61
     1 % bbb.sty  10-Nov-1991, 27-Mar-1994
       
     2 %
     1 %
     3 % blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
     2 % 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
     4 %
     3 %
     5 
     4 
     6 \def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
     5 \def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
     7 \def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
     6 \def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
     8 \def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
     7 \def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}