src/HOL/String.thy
changeset 52435 6646bb548c6b
parent 52365 95186e6e4bf4
child 52910 7bfe0df532a9
     1.1 --- a/src/HOL/String.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/String.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -400,24 +400,25 @@
     1.4  code_reserved OCaml string
     1.5  code_reserved Scala string
     1.6  
     1.7 -code_type literal
     1.8 -  (SML "string")
     1.9 -  (OCaml "string")
    1.10 -  (Haskell "String")
    1.11 -  (Scala "String")
    1.12 +code_printing
    1.13 +  type_constructor literal \<rightharpoonup>
    1.14 +    (SML) "string"
    1.15 +    and (OCaml) "string"
    1.16 +    and (Haskell) "String"
    1.17 +    and (Scala) "String"
    1.18  
    1.19  setup {*
    1.20    fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
    1.21  *}
    1.22  
    1.23 -code_instance literal :: equal
    1.24 -  (Haskell -)
    1.25 -
    1.26 -code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
    1.27 -  (SML "!((_ : string) = _)")
    1.28 -  (OCaml "!((_ : string) = _)")
    1.29 -  (Haskell infix 4 "==")
    1.30 -  (Scala infixl 5 "==")
    1.31 +code_printing
    1.32 +  class_instance literal :: equal \<rightharpoonup>
    1.33 +    (Haskell) -
    1.34 +| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
    1.35 +    (SML) "!((_ : string) = _)"
    1.36 +    and (OCaml) "!((_ : string) = _)"
    1.37 +    and (Haskell) infix 4 "=="
    1.38 +    and (Scala) infixl 5 "=="
    1.39  
    1.40  hide_type (open) literal
    1.41