src/HOL/String.thy
changeset 49948 744934b818c7
parent 49834 b27bbb021df1
child 49972 f11f8905d9fd
     1.1 --- a/src/HOL/String.thy	Sat Oct 20 09:09:37 2012 +0200
     1.2 +++ b/src/HOL/String.thy	Sat Oct 20 09:12:16 2012 +0200
     1.3 @@ -149,6 +149,14 @@
     1.4    Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
     1.5    Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
     1.6  
     1.7 +lemma UNIV_set_chars:
     1.8 +  "UNIV = set chars"
     1.9 +  by (simp only: UNIV_char UNIV_nibble) code_simp
    1.10 +
    1.11 +lemma distinct_chars:
    1.12 +  "distinct chars"
    1.13 +  by code_simp
    1.14 +
    1.15  
    1.16  subsection {* Strings as dedicated type *}
    1.17  
    1.18 @@ -213,3 +221,4 @@
    1.19  hide_type (open) literal
    1.20  
    1.21  end
    1.22 +