# HG changeset patch
# User wenzelm
# Date 969029097 -7200
# Node ID 5eec17e4e95e31feb6d6374f5d1e767e9eb2aea0
# Parent  fd5053c8a7acdfa9741225c0da3d7da38e329d25
added latexsym (no longer loaded by isabellesym);

diff -r fd5053c8a7ac -r 5eec17e4e95e src/HOL/MicroJava/document/root.tex
--- a/src/HOL/MicroJava/document/root.tex	Fri Sep 15 16:40:20 2000 +0200
+++ b/src/HOL/MicroJava/document/root.tex	Fri Sep 15 16:44:57 2000 +0200
@@ -1,6 +1,6 @@
 
 \documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym,pdfsetup}
+\usepackage{latexsym,isabelle,isabellesym,pdfsetup}
 
 \pagestyle{myheadings}