src/HOL/Library/Code_Char.thy
changeset 25965 05df64f786a4
parent 24999 1dbe785ed529
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:53:58 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Jan 25 14:54:41 2008 +0100
     1.3 @@ -9,6 +9,16 @@
     1.4  imports List
     1.5  begin
     1.6  
     1.7 +declare char.recs [code func del] char.cases [code func del]
     1.8 +
     1.9 +lemma [code func]:
    1.10 +  "size (c\<Colon>char) = 0"
    1.11 +  by (cases c) simp
    1.12 +
    1.13 +lemma [code func]:
    1.14 +  "char_size (c\<Colon>char) = 0"
    1.15 +  by (cases c) simp
    1.16 +
    1.17  code_type char
    1.18    (SML "char")
    1.19    (OCaml "char")