tuned;
authorwenzelm
Sat Oct 30 20:32:04 1999 +0200 (1999-10-30)
changeset 798486c0cc789f61
parent 7983 d823fdcc0645
child 7985 e6fcb279fdbe
tuned;
src/HOL/Real/HahnBanach/document/bbb.sty
src/HOL/Real/HahnBanach/document/notation.tex
src/HOL/Real/HahnBanach/document/root.tex
     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