doc-src/Intro/intro.tex

-\documentstyle[a4,12pt,proof,iman,alltt]{article}
+\documentstyle[a4,12pt,proof,iman,extra]{article}
 %% $Id$
 %% run    bibtex intro         to prepare bibliography
 %% run    ../sedindex intro    to prepare index file
 %prth *(\(.*\));          \1;      
 %{\\out \(.*\)}          {\\out val it = "\1" : thm}

 support many-sorted and higher-order logics.  The current version provides
 greater support for theories and is much faster.  Isabelle is still under
 development and will continue to change.
 
 \subsubsection*{Overview} 
-This manual consists of three parts.  
-Part~I discusses the Isabelle's foundations.
-Part~II, presents simple on-line sessions, starting with forward proof.
-It also covers basic tactics and tacticals, and some commands for invoking
-Part~III contains further examples for users with a bit of experience.
-It explains how to derive rules define theories, and concludes with an
-extended example: a Prolog interpreter.
+This manual consists of three parts.  Part~I discusses the Isabelle's
+foundations.  Part~II, presents simple on-line sessions, starting with
+forward proof.  It also covers basic tactics and tacticals, and some
+commands for invoking them.  Part~III contains further examples for users
+with a bit of experience.  It explains how to derive rules define theories,
+and concludes with an extended example: a Prolog interpreter.
 
 Isabelle's Reference Manual and Object-Logics manual contain more details.
 They assume familiarity with the concepts presented here.
 
 

 \clearfirst  \pagestyle{headings}
 \include{foundations}
 \include{getting}
 \include{advanced}
 
-
 \bibliographystyle{plain} \small\raggedright\frenchspacing
-\bibliography{atp,funprog,general,logicprog,theory}
+\bibliography{string,atp,funprog,general,logicprog,theory}
 
 \input{intro.ind}
 \end{document}