src/HOL/HOL.thy
changeset 26747 f32fa5f5bdd1
parent 26739 947b6013e863
child 26957 e3f04fdd994d
     1.1 --- a/src/HOL/HOL.thy	Thu Apr 24 11:38:42 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Apr 24 16:53:04 2008 +0200
     1.3 @@ -1699,7 +1699,7 @@
     1.4    CodeUnit.add_const_alias @{thm equals_eq}
     1.5    #> CodeName.setup
     1.6    #> CodeTarget.setup
     1.7 -  #> Nbe.setup @{sort eq} [(@{const_name eq_class.eq}, @{const_name "op ="})]
     1.8 +  #> Nbe.setup
     1.9  *}
    1.10  
    1.11  lemma [code func]: