# HG changeset patch
# User wenzelm
# Date 941308324 -7200
# Node ID 86c0cc789f613e56904f798413296a2eb56590df
# Parent  d823fdcc0645b56c3c680d2b029fffd6b860329c
tuned;

diff -r d823fdcc0645 -r 86c0cc789f61 src/HOL/Real/HahnBanach/document/bbb.sty
--- 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}}}
diff -r d823fdcc0645 -r 86c0cc789f61 src/HOL/Real/HahnBanach/document/notation.tex
--- 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}
diff -r d823fdcc0645 -r 86c0cc789f61 src/HOL/Real/HahnBanach/document/root.tex
--- 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}