1.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Mon Oct 11 21:05:01 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Mon Oct 11 21:10:50 2010 +0100
     1.3 @@ -619,7 +619,7 @@
     1.4    "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text
     1.5    "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by
     1.6    primitive recursion over the syntactic structure of a single type
     1.7 -  argument.
     1.8 +  argument.  See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.
     1.9  *}
    1.10  
    1.11  text %mlref {*