1.1 --- a/doc-src/Intro/intro.tex	Wed Mar 23 16:56:44 1994 +0100
     1.2 +++ b/doc-src/Intro/intro.tex	Thu Mar 24 13:25:12 1994 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -\documentstyle[a4,12pt,proof,iman,alltt]{article}
     1.5 +\documentstyle[a4,12pt,proof,iman,extra]{article}
     1.6  %% $Id$
     1.7  %% run    bibtex intro         to prepare bibliography
     1.8  %% run    ../sedindex intro    to prepare index file
     1.9 @@ -95,13 +95,12 @@
    1.10  development and will continue to change.
    1.11  
    1.12  \subsubsection*{Overview} 
    1.13 -This manual consists of three parts.  
    1.14 -Part~I discusses the Isabelle's foundations.
    1.15 -Part~II, presents simple on-line sessions, starting with forward proof.
    1.16 -It also covers basic tactics and tacticals, and some commands for invoking
    1.17 -Part~III contains further examples for users with a bit of experience.
    1.18 -It explains how to derive rules define theories, and concludes with an
    1.19 -extended example: a Prolog interpreter.
    1.20 +This manual consists of three parts.  Part~I discusses the Isabelle's
    1.21 +foundations.  Part~II, presents simple on-line sessions, starting with
    1.22 +forward proof.  It also covers basic tactics and tacticals, and some
    1.23 +commands for invoking them.  Part~III contains further examples for users
    1.24 +with a bit of experience.  It explains how to derive rules define theories,
    1.25 +and concludes with an extended example: a Prolog interpreter.
    1.26  
    1.27  Isabelle's Reference Manual and Object-Logics manual contain more details.
    1.28  They assume familiarity with the concepts presented here.
    1.29 @@ -142,9 +141,8 @@
    1.30  \include{getting}
    1.31  \include{advanced}
    1.32  
    1.33 -
    1.34  \bibliographystyle{plain} \small\raggedright\frenchspacing
    1.35 -\bibliography{atp,funprog,general,logicprog,theory}
    1.36 +\bibliography{string,atp,funprog,general,logicprog,theory}
    1.37  
    1.38  \input{intro.ind}
    1.39  \end{document}