diff -r 33a46e6c7f04 -r cc2be3315e72 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 02 15:43:15 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 02 15:43:16 2007 +0100 @@ -749,8 +749,7 @@ consts "op =" :: "'a" (*>*) -axclass eq \ type - (attach "op =") +class eq (attach "op =") = notes reflexive text {* This merely introduces a class @{text eq} with corresponding