# HG changeset patch # User nipkow # Date 1412019288 -7200 # Node ID d5f24630c10454810bd7dcfd81c00ece75b667cc # Parent 7836013951e6d9497608decc80952498c8cbebf7 tuned diff -r 7836013951e6 -r d5f24630c104 src/Doc/Prog_Prove/document/intro-isabelle.tex --- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Mon Sep 29 18:37:33 2014 +0200 +++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Mon Sep 29 21:34:48 2014 +0200 @@ -1,5 +1,5 @@ Isabelle is a generic system for -implementing logical formalisms, and Isabelle/HOL is the specialization +implementing logical formalisms, and Isabelle/HOL is the specialisation 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}. \]