Quotient-Paper/Paper.thy
changeset 2257 d40031f786f0
parent 2256 f5f21feaa168
child 2258 72ce58b76c3b
equal deleted inserted replaced
2256:f5f21feaa168 2257:d40031f786f0
   255   and Section \ref{sec:conc} concludes and compares our results to existing 
   255   and Section \ref{sec:conc} concludes and compares our results to existing 
   256   work.
   256   work.
   257 *}
   257 *}
   258 
   258 
   259 
   259 
   260 section {* Preliminaries and General Quotient\label{sec:prelims} *}
   260 section {* Preliminaries and General Quotients\label{sec:prelims} *}
   261 
   261 
   262 text {*
   262 text {*
   263   We describe here briefly some of the most basic concepts of HOL 
   263   We describe here briefly some of the most basic concepts of HOL 
   264   we rely on and some of the important definitions given by Homeier 
   264   we rely on and some of the important definitions given by Homeier 
   265   \cite{Homeier05}. 
   265   \cite{Homeier05}.