src/HOL/Datatype.thy
changeset 19787 b949911ecff5
parent 19770 be5c23ebe1eb
child 19817 bb16bf9ae3fd
     1.1 --- a/src/HOL/Datatype.thy	Tue Jun 06 14:55:56 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Tue Jun 06 14:56:42 2006 +0200
     1.3 @@ -218,6 +218,17 @@
     1.4    apply (simp split add: sum.split)
     1.5    done
     1.6  
     1.7 +
     1.8 +consts
     1.9 +  is_none :: "'a option \<Rightarrow> bool"
    1.10 +primrec
    1.11 +  "is_none None = True"
    1.12 +  "is_none (Some x) = False"
    1.13 +
    1.14 +(* lemma is_none_none [code unfolt]:
    1.15 +  "(x = None) = (is_none x)" 
    1.16 +by (cases "x") simp_all *)
    1.17 +
    1.18  lemmas [code] = imp_conv_disj
    1.19  
    1.20  subsubsection {* Codegenerator setup *}