--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Sep 30 16:40:03 2014 +0200
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Sep 30 18:44:01 2014 +0200
@@ -1,5 +1,5 @@
Isabelle is a generic system for
-implementing logical formalisms, and Isabelle/HOL is the specialisation
+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}. \]