src/HOL/String.thy
changeset 57437 0baf08c075b9
parent 57247 8191ccf6a1bd
child 57512 cc97b347b301
     1.1 --- a/src/HOL/String.thy	Sun Jun 29 21:07:53 2014 +0200
     1.2 +++ b/src/HOL/String.thy	Mon Jun 30 08:00:36 2014 +0200
     1.3 @@ -358,6 +358,10 @@
     1.4  
     1.5  setup_lifting (no_code) type_definition_literal
     1.6  
     1.7 +definition implode :: "string \<Rightarrow> String.literal"
     1.8 +where
     1.9 +  "implode = STR"
    1.10 +
    1.11  instantiation literal :: size
    1.12  begin
    1.13  
    1.14 @@ -440,4 +444,6 @@
    1.15  
    1.16  hide_type (open) literal
    1.17  
    1.18 +hide_const (open) implode explode
    1.19 +
    1.20  end