| changeset 22385 | cc2be3315e72 |
| parent 22292 | 3b118010ec08 |
| child 22423 | c1836b14c63a |
--- 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 \<subseteq> type - (attach "op =") +class eq (attach "op =") = notes reflexive text {* This merely introduces a class @{text eq} with corresponding