diff -r 660ffb526069 -r 71a8ac5d039f src/Doc/Classes/Classes.thy --- a/src/Doc/Classes/Classes.thy Wed Apr 23 17:57:56 2014 +0200 +++ b/src/Doc/Classes/Classes.thy Thu Apr 24 00:08:48 2014 +0200 @@ -175,7 +175,7 @@ end %quote text {* - \noindent Note the occurence of the name @{text mult_nat} in the + \noindent Note the occurrence of the name @{text mult_nat} in the primrec declaration; by default, the local name of a class operation @{text f} to be instantiated on type constructor @{text \} is mangled as @{text f_\}. In case of uncertainty, these names may be