src/HOL/Real/HahnBanach/document/bbb.sty
changeset 7984 86c0cc789f61
parent 7978 1b99ee57d131
     1.1 --- a/src/HOL/Real/HahnBanach/document/bbb.sty	Sat Oct 30 20:21:46 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/document/bbb.sty	Sat Oct 30 20:32:04 1999 +0200
     1.3 @@ -1,6 +1,5 @@
     1.4 -% bbb.sty  10-Nov-1991, 27-Mar-1994
     1.5  %
     1.6 -% blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
     1.7 +% 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
     1.8  %
     1.9  
    1.10  \def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}