
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 \<subseteq> type
-  (attach "op =")
+class eq (attach "op =") = notes reflexive
 
 text {*
   This merely introduces a class @{text eq} with corresponding




