diff -r 5ac498bffb6b -r 71015f46b3c1 src/HOL/MicroJava/document/introduction.tex --- a/src/HOL/MicroJava/document/introduction.tex Thu Feb 21 11:05:20 2002 +0100 +++ b/src/HOL/MicroJava/document/introduction.tex Thu Feb 21 13:37:09 2002 +0100 @@ -1,5 +1,6 @@ +\chapter{Preface} -\section*{Introduction} +\section{Introduction} \label{sec:introduction} This document contains the automatically generated listings of the