removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;
\index{model checking example|(}%
\index{lfp@{\texttt{lfp}}!applications of|see{CTL}}
\input{CTL/document/Base.tex}
\input{CTL/document/PDL.tex}
\input{CTL/document/CTL.tex}
\index{model checking example|)}