src/HOL/Code_Generator.thy
changeset 22473 753123c89d72
parent 22423 c1836b14c63a
child 22480 b20bc8029edb
     1.1 --- a/src/HOL/Code_Generator.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4  
     1.5  text {* operational equality for code generation *}
     1.6  
     1.7 -class eq (attach "op =") = notes reflexive
     1.8 +class eq (attach "op =") = type
     1.9  
    1.10  
    1.11  text {* equality for Haskell *}