changeset 25965 | 05df64f786a4 |
parent 25762 | c03e9d04b3e4 |
child 26150 | f6bd8686b71e |
--- a/src/HOL/Set.thy Fri Jan 25 14:53:58 2008 +0100 +++ b/src/HOL/Set.thy Fri Jan 25 14:54:41 2008 +0100 @@ -2141,7 +2141,7 @@ definition is_empty :: "'a set \<Rightarrow> bool" where - [code func del]: "is_empty A \<longleftrightarrow> A = {}" + [code func del, code post]: "is_empty A \<longleftrightarrow> A = {}" lemmas [code inline] = is_empty_def [symmetric] lemma is_empty_insert [code func]: