src/HOL/Datatype.thy
changeset 22886 cdff6ef76009
parent 22782 8bc6fbbe1d0f
child 24162 8dfd5dd65d82
     1.1 --- a/src/HOL/Datatype.thy	Wed May 09 07:53:04 2007 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed May 09 07:53:06 2007 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  
     1.5  (** apfst -- can be used in similar type definitions **)
     1.6  
     1.7 -lemma apfst_conv [simp, code func]: "apfst f (a, b) = (f a, b)"
     1.8 +lemma apfst_conv [simp, code]: "apfst f (a, b) = (f a, b)"
     1.9  by (simp add: apfst_def)
    1.10  
    1.11  
    1.12 @@ -715,12 +715,12 @@
    1.13  
    1.14  constdefs
    1.15    option_map :: "('a => 'b) => ('a option => 'b option)"
    1.16 -  "option_map == %f y. case y of None => None | Some x => Some (f x)"
    1.17 +  [code func del]: "option_map == %f y. case y of None => None | Some x => Some (f x)"
    1.18  
    1.19 -lemma option_map_None [simp, code func]: "option_map f None = None"
    1.20 +lemma option_map_None [simp, code]: "option_map f None = None"
    1.21    by (simp add: option_map_def)
    1.22  
    1.23 -lemma option_map_Some [simp, code func]: "option_map f (Some x) = Some (f x)"
    1.24 +lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)"
    1.25    by (simp add: option_map_def)
    1.26  
    1.27  lemma option_map_is_None [iff]:
    1.28 @@ -742,13 +742,9 @@
    1.29  
    1.30  subsubsection {* Code generator setup *}
    1.31  
    1.32 -lemmas [code] = fst_conv snd_conv imp_conv_disj
    1.33 -
    1.34  definition
    1.35    is_none :: "'a option \<Rightarrow> bool" where
    1.36 -  is_none_none [normal post, symmetric]: "is_none x \<longleftrightarrow> x = None"
    1.37 -
    1.38 -lemmas [code inline] = is_none_none
    1.39 +  is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    1.40  
    1.41  lemma is_none_code [code]:
    1.42    shows "is_none None \<longleftrightarrow> True"