src/Doc/Tutorial/Types/Axioms.thy

 Table~\ref{tab:overloading} in the appendix.  Section
 \ref{sec:numeric-classes} covers a range of corresponding classes
 \emph{with} axioms.
 
 Further note that classes may contain axioms but \emph{no} operations.
-An example is class @{class finite} from theory @{theory Finite_Set}
+An example is class @{class finite} from theory @{theory "HOL.Finite_Set"}
 which specifies a type to be finite: @{lemma [source] "finite (UNIV :: 'a::finite
 set)" by (fact finite_UNIV)}.\<close>
 
 (*<*)end(*>*)