# HG changeset patch # User blanchet # Date 1398290928 -7200 # Node ID 71a8ac5d039f5271e4c89c472b5a41486312a037 # Parent 660ffb5260696c3ac459776886c200b11126f3b6 spelling 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