Theory Renaming2_String

subsection ‹Renaming strings apart›

theory Renaming2_String
  imports 
    Renaming2
    Lists_are_Infinite
begin

lift_definition string_rename :: "string renaming2" is "(Cons (CHR ''x''), Cons (CHR ''y''))" 
  by auto

end