src/HOL/String.thy
changeset 31205 98370b26c2ce
parent 31176 92e0ed53db25
child 31484 cabcb95fde29
     1.1 --- a/src/HOL/String.thy	Tue May 19 13:57:51 2009 +0200
     1.2 +++ b/src/HOL/String.thy	Tue May 19 16:54:55 2009 +0200
     1.3 @@ -85,15 +85,14 @@
     1.4  
     1.5  subsection {* Strings as dedicated datatype *}
     1.6  
     1.7 -datatype message_string = STR string
     1.8 +datatype literal = STR string
     1.9  
    1.10 -lemmas [code del] =
    1.11 -  message_string.recs message_string.cases
    1.12 +lemmas [code del] = literal.recs literal.cases
    1.13  
    1.14 -lemma [code]: "size (s\<Colon>message_string) = 0"
    1.15 +lemma [code]: "size (s\<Colon>literal) = 0"
    1.16    by (cases s) simp_all
    1.17  
    1.18 -lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
    1.19 +lemma [code]: "literal_size (s\<Colon>literal) = 0"
    1.20    by (cases s) simp_all
    1.21  
    1.22  
    1.23 @@ -101,19 +100,19 @@
    1.24  
    1.25  use "Tools/string_code.ML"
    1.26  
    1.27 -code_type message_string
    1.28 +code_type literal
    1.29    (SML "string")
    1.30    (OCaml "string")
    1.31    (Haskell "String")
    1.32  
    1.33  setup {*
    1.34 -  fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
    1.35 +  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
    1.36  *}
    1.37  
    1.38 -code_instance message_string :: eq
    1.39 +code_instance literal :: eq
    1.40    (Haskell -)
    1.41  
    1.42 -code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
    1.43 +code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
    1.44    (SML "!((_ : string) = _)")
    1.45    (OCaml "!((_ : string) = _)")
    1.46    (Haskell infixl 4 "==")
    1.47 @@ -147,4 +146,6 @@
    1.48  in Codegen.add_codegen "char_codegen" char_codegen end
    1.49  *}
    1.50  
    1.51 +hide (open) type literal
    1.52 +
    1.53  end
    1.54 \ No newline at end of file