more glyphs proposed by Simon Foster: 0x002713, 0x002717, 0x002af4, 0x002afb, 0x002afd;
corresponding symbols and latex macros;
\documentclass[envcountsame,envcountchap]{svmono}
\input{prelude}
\newif\ifsem
\begin{document}
\title{Programming and Proving in Isabelle/HOL}
\subtitle{\includegraphics[scale=.7]{isabelle_hol}}
\author{Tobias Nipkow}
\maketitle
\frontmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\setcounter{tocdepth}{1}
\tableofcontents
\mainmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\part{Isabelle}
\chapter{Introduction}
\input{intro-isabelle.tex}
\chapter{Programming and Proving}
\label{sec:FP}
\input{Basics.tex}
\input{Bool_nat_list}
\input{Types_and_funs}
%\chapter{Case Study: IMP Expressions}
%\label{sec:CaseStudyExp}
%\input{../generated/Expressions}
\chapter{Logic and Proof Beyond Equality}
\label{ch:Logic}
\input{Logic}
\chapter{Isar: A Language for Structured Proofs}
\label{ch:Isar}
\input{Isar}
\backmatter%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliographystyle{plain}
\bibliography{root}
%\printindex
\end{document}