| changeset 22424 | 8a5412121687 |
| parent 22230 | bdec4a82f385 |
| child 22632 | 59c117a0bcf3 |
--- a/src/HOL/Datatype.thy Fri Mar 09 08:45:53 2007 +0100 +++ b/src/HOL/Datatype.thy Fri Mar 09 08:45:55 2007 +0100 @@ -726,7 +726,9 @@ definition is_none :: "'a option \<Rightarrow> bool" where - is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None" + is_none_none [normal post, symmetric]: "is_none x \<longleftrightarrow> x = None" + +lemmas [code inline] = is_none_none lemma is_none_code [code]: shows "is_none None \<longleftrightarrow> True"