src/HOL/Datatype.thy
changeset 21404 eb85850d3eb7
parent 21243 afffe1f72143
child 21407 af60523da908
     1.1 --- a/src/HOL/Datatype.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -726,7 +726,7 @@
     1.4  subsubsection {* Code generator setup *}
     1.5  
     1.6  definition
     1.7 -  is_none :: "'a option \<Rightarrow> bool"
     1.8 +  is_none :: "'a option \<Rightarrow> bool" where
     1.9    is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
    1.10  
    1.11  lemma is_none_code [code]: