src/HOL/Real/HahnBanach/document/bbb.sty
author wenzelm
Sat, 30 Oct 1999 20:32:04 +0200
changeset 7984 86c0cc789f61
parent 7978 1b99ee57d131
permissions -rw-r--r--
tuned;
     1 %
     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
     3 %
     4 
     5 \def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
     6 \def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
     7 \def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
     8 \def\bbbE{{{\rm I}\mkern-3.8mu{\rm E}}}
     9 \def\bbbF{{{\rm I}\mkern-3.8mu{\rm F}}}
    10 \def\bbbG{{{\rm G}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
    11 \def\bbbH{{{\rm I}\mkern-3.8mu{\rm H}}}
    12 \def\bbbI{{{\rm I}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
    13 \def\bbbJ{{{\rm J}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
    14 \def\bbbK{{{\rm I}\mkern-3.8mu{\rm K}}}
    15 \def\bbbL{{{\rm I}\mkern-3.8mu{\rm L}}}
    16 \def\bbbM{{{\rm I}\mkern-3.8mu{\rm M}}}
    17 \def\bbbN{{{\rm I}\mkern-3.8mu{\rm N}}}
    18 \def\bbbO{{{\rm O}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
    19 \def\bbbP{{{\rm I}\mkern-3.8mu{\rm P}}}
    20 \def\bbbQ{{{\rm Q}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
    21 \def\bbbR{{{\rm I}\mkern-3.8mu{\rm R}}}
    22 \def\bbbT{{{\rm T}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
    23 \def\bbbU{{{\rm U}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
    24 \def\bbbZ{{{\sf Z}\mkern-7.5mu{\sf Z}}}