src/HOL/Library/Code_Char.thy
changeset 38857 97775f3e8722
parent 37459 7a3610dca96b
child 39250 548a3e5521ab
     1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    #> String_Code.add_literal_list_string "Haskell"
     1.5  *}
     1.6  
     1.7 -code_instance char :: eq
     1.8 +code_instance char :: equal
     1.9    (Haskell -)
    1.10  
    1.11  code_reserved SML
    1.12 @@ -31,7 +31,7 @@
    1.13  code_reserved Scala
    1.14    char
    1.15  
    1.16 -code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.17 +code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.18    (SML "!((_ : char) = _)")
    1.19    (OCaml "!((_ : char) = _)")
    1.20    (Haskell infixl 4 "==")