src/HOL/MicroJava/document/root.tex
changeset 55369 713629c2b73c
parent 17159 d5060118122e
child 58886 8a6cac7c7247
equal deleted inserted replaced
55368:ec7dae620736 55369:713629c2b73c
     1 % $Id$
       
     2 
       
     3 %\documentclass[11pt,a4paper]{article}
       
     4 \documentclass[11pt,a4paper]{book}
     1 \documentclass[11pt,a4paper]{book}
     5 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
     2 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
     6 
     3 
     7 \urlstyle{rm}
     4 \urlstyle{rm}
     8 \pagestyle{myheadings}
     5 \pagestyle{myheadings}