src/HOL/String.thy
changeset 33237 565ad811db21
parent 33063 4d462963a7db
child 34886 873c31d9f10d
     1.1 --- a/src/HOL/String.thy	Tue Oct 27 15:32:21 2009 +0100
     1.2 +++ b/src/HOL/String.thy	Tue Oct 27 15:32:21 2009 +0100
     1.3 @@ -155,7 +155,7 @@
     1.4  
     1.5  datatype literal = STR string
     1.6  
     1.7 -lemmas [code del] = literal.recs literal.cases
     1.8 +declare literal.cases [code del] literal.recs [code del]
     1.9  
    1.10  lemma [code]: "size (s\<Colon>literal) = 0"
    1.11    by (cases s) simp_all
    1.12 @@ -168,6 +168,9 @@
    1.13  
    1.14  use "Tools/string_code.ML"
    1.15  
    1.16 +code_reserved SML string
    1.17 +code_reserved OCaml string
    1.18 +
    1.19  code_type literal
    1.20    (SML "string")
    1.21    (OCaml "string")
    1.22 @@ -185,9 +188,6 @@
    1.23    (OCaml "!((_ : string) = _)")
    1.24    (Haskell infixl 4 "==")
    1.25  
    1.26 -code_reserved SML string
    1.27 -code_reserved OCaml string
    1.28 -
    1.29  
    1.30  types_code
    1.31    "char" ("string")