src/HOL/Code_Message.thy

replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
minor tuning according to Isabelle coding conventions;

(*  ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen
*)

header {* Monolithic strings (message strings) for code generation *}

theory Code_Message
imports Plain "~~/src/HOL/List"
begin

subsection {* Datatype of messages *}

datatype message_string = STR string

lemmas [code del] = message_string.recs message_string.cases

lemma [code]: "size (s\<Colon>message_string) = 0"
  by (cases s) simp_all

lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
  by (cases s) simp_all

subsection {* ML interface *}

ML {*
structure Message_String =
struct

fun mk s = @{term STR} $ HOLogic.mk_string s;

end;
*}


subsection {* Code serialization *}

code_type message_string
  (SML "string")
  (OCaml "string")
  (Haskell "String")

setup {*
  fold (fn target => add_literal_message @{const_name STR} target)
    ["SML", "OCaml", "Haskell"]
*}

code_reserved SML string
code_reserved OCaml string

code_instance message_string :: eq
  (Haskell -)

code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
  (SML "!((_ : string) = _)")
  (OCaml "!((_ : string) = _)")
  (Haskell infixl 4 "==")

end