src/HOL/Real/HahnBanach/document/root.tex
changeset 7984 86c0cc789f61
parent 7978 1b99ee57d131
child 8585 8a3ae21e4a5b
equal deleted inserted replaced
7983:d823fdcc0645 7984:86c0cc789f61
     1 
     1 
     2 \documentclass[11pt,a4paper,twoside]{article}
     2 \documentclass[11pt,a4paper,twoside]{article}
     3 
     3 
     4 \usepackage{comment}
     4 \usepackage{comment}
     5 \usepackage{latexsym,theorem}
     5 \usepackage{latexsym,theorem}
     6 \usepackage{isabelle,pdfsetup} %last one!
     6 \usepackage{isabelle,isabellesym,bbb}
     7 \usepackage{bbb}
     7 \usepackage{pdfsetup} %last one!
     8 
     8 
     9 \input{notation}
     9 \input{notation}
    10 
    10 
    11 \begin{document}
    11 \begin{document}
    12 
    12