src/HOL/String.thy
changeset 56846 9df717fef2bb
parent 55969 8820ddb8f9f4
child 57247 8191ccf6a1bd
     1.1 --- a/src/HOL/String.thy	Sun May 04 16:17:53 2014 +0200
     1.2 +++ b/src/HOL/String.thy	Sun May 04 18:14:58 2014 +0200
     1.3 @@ -20,10 +20,9 @@
     1.4  qed
     1.5  
     1.6  lemma size_nibble [code, simp]:
     1.7 -  "size (x::nibble) = 0" by (cases x) simp_all
     1.8 -
     1.9 -lemma nibble_size [code, simp]:
    1.10 -  "nibble_size (x::nibble) = 0" by (cases x) simp_all
    1.11 +  "size_nibble (x::nibble) = 0"
    1.12 +  "size (x::nibble) = 0"
    1.13 +  by (cases x, simp_all)+
    1.14  
    1.15  instantiation nibble :: enum
    1.16  begin
    1.17 @@ -136,10 +135,9 @@
    1.18  qed
    1.19  
    1.20  lemma size_char [code, simp]:
    1.21 -  "size (c::char) = 0" by (cases c) simp
    1.22 -
    1.23 -lemma char_size [code, simp]:
    1.24 -  "char_size (c::char) = 0" by (cases c) simp
    1.25 +  "size_char (c::char) = 0"
    1.26 +  "size (c::char) = 0"
    1.27 +  by (cases c, simp)+
    1.28  
    1.29  instantiation char :: enum
    1.30  begin