src/Doc/Prog_Prove/document/intro-isabelle.tex

 Isabelle is a generic system for
 implementing logical formalisms, and Isabelle/HOL is the specialization
 of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce
 HOL step by step following the equation
 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
-We assume that the reader is used to logical and set theoretic notation
+We assume that the reader is used to logical and set-theoretic notation
 and is familiar with the basic concepts of functional programming.
 \ifsem
 Open-minded readers have been known to pick up functional
 programming through the wealth of examples in \autoref{sec:FP}
 and \autoref{sec:CaseStudyExp}.

 \autoref{sec:CaseStudyExp} contains a
 small case study: arithmetic and boolean expressions, their evaluation,
 optimization and compilation.
 \fi
 \autoref{ch:Logic} introduces the rest of HOL: the
-language of formulas beyond equality, automatic proof tools, single
-step proofs, and inductive definitions, an essential specification construct.
+language of formulas beyond equality, automatic proof tools, single-step
+proofs, and inductive definitions, an essential specification construct.
 \autoref{ch:Isar} introduces Isar, Isabelle's language for writing structured
 proofs.
 
 %Further material (slides, demos etc) can be found online at
 %\url{http://www.in.tum.de/~nipkow}.