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

     2.1 --- a/src/HOL/Real/HahnBanach/document/notation.tex	Sat Oct 30 20:21:46 1999 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/document/notation.tex	Sat Oct 30 20:32:04 1999 +0200
     2.3 @@ -1,10 +1,8 @@
     2.4  
     2.5  \renewcommand{\isamarkupheader}[1]{\section{#1}}
     2.6 -\newcommand{\isasymlambda}{${\mathtt{\lambda}}$}
     2.7  \newcommand{\isasymprod}{\emph{$\mult$}}
     2.8  \newcommand{\isasymzero}{\emph{$\zero$}}
     2.9  
    2.10 -
    2.11  \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
    2.12  \newcommand{\var}[1]{{?\!#1}}
    2.13  \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}

     3.1 --- a/src/HOL/Real/HahnBanach/document/root.tex	Sat Oct 30 20:21:46 1999 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/document/root.tex	Sat Oct 30 20:32:04 1999 +0200
     3.3 @@ -3,8 +3,8 @@
     3.4  
     3.5  \usepackage{comment}
     3.6  \usepackage{latexsym,theorem}
     3.7 -\usepackage{isabelle,pdfsetup} %last one!
     3.8 -\usepackage{bbb}
     3.9 +\usepackage{isabelle,isabellesym,bbb}
    3.10 +\usepackage{pdfsetup} %last one!
    3.11  
    3.12  \input{notation}
    3.13