src/HOL/String.thy
changeset 38857 97775f3e8722
parent 37743 0a3fa8fbcdc5
child 38858 1920158cfa17
     1.1 --- a/src/HOL/String.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/String.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -183,10 +183,10 @@
     1.4    fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
     1.5  *}
     1.6  
     1.7 -code_instance literal :: eq
     1.8 +code_instance literal :: equal
     1.9    (Haskell -)
    1.10  
    1.11 -code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
    1.12 +code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
    1.13    (SML "!((_ : string) = _)")
    1.14    (OCaml "!((_ : string) = _)")
    1.15    (Haskell infixl 4 "==")