src/HOL/Datatype.thy
changeset 20105 454f4be984b7
parent 19890 1aad48bcc674
child 20453 855f07fabd76
     1.1 --- a/src/HOL/Datatype.thy	Wed Jul 12 00:34:54 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Jul 12 17:00:22 2006 +0200
     1.3 @@ -227,9 +227,9 @@
     1.4    "is_none None = True"
     1.5    "is_none (Some x) = False"
     1.6  
     1.7 -lemma is_none_none [code unfolt]:
     1.8 +lemma is_none_none [code inline]:
     1.9    "(x = None) = (is_none x)" 
    1.10 -by (cases "x") simp_all
    1.11 +by (cases x) simp_all
    1.12  
    1.13  lemmas [code] = imp_conv_disj
    1.14  
    1.15 @@ -257,6 +257,10 @@
    1.16    fst_conv [code]
    1.17    snd_conv [code]
    1.18  
    1.19 +lemma split_is_prod_case [code inline]:
    1.20 +  "split = prod_case"
    1.21 +by (simp add: expand_fun_eq split_def prod.cases)
    1.22 +
    1.23  code_typapp bool
    1.24    ml (target_atom "bool")
    1.25    haskell (target_atom "Bool")