--- a/src/HOL/Real/HahnBanach/document/bbb.sty Sat Oct 30 20:21:46 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/bbb.sty Sat Oct 30 20:32:04 1999 +0200
@@ -1,6 +1,5 @@
-% bbb.sty 10-Nov-1991, 27-Mar-1994
%
-% blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
+% 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}}}
--- a/src/HOL/Real/HahnBanach/document/notation.tex Sat Oct 30 20:21:46 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Sat Oct 30 20:32:04 1999 +0200
@@ -1,10 +1,8 @@
\renewcommand{\isamarkupheader}[1]{\section{#1}}
-\newcommand{\isasymlambda}{${\mathtt{\lambda}}$}
\newcommand{\isasymprod}{\emph{$\mult$}}
\newcommand{\isasymzero}{\emph{$\zero$}}
-
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
\newcommand{\var}[1]{{?\!#1}}
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
--- a/src/HOL/Real/HahnBanach/document/root.tex Sat Oct 30 20:21:46 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex Sat Oct 30 20:32:04 1999 +0200
@@ -3,8 +3,8 @@
\usepackage{comment}
\usepackage{latexsym,theorem}
-\usepackage{isabelle,pdfsetup} %last one!
-\usepackage{bbb}
+\usepackage{isabelle,isabellesym,bbb}
+\usepackage{pdfsetup} %last one!
\input{notation}