| changeset 25164 | 0fcb4775cbfb |
| parent 24728 | e2b3a1065676 |
| child 25193 | e2e1a4b00de3 |
--- a/src/HOL/IntDef.thy Wed Oct 24 07:19:52 2007 +0200 +++ b/src/HOL/IntDef.thy Wed Oct 24 07:19:53 2007 +0200 @@ -384,7 +384,7 @@ definition neg :: "'a\<Colon>ordered_idom \<Rightarrow> bool" where - [code inline]: "neg Z \<longleftrightarrow> Z < 0" + "neg Z \<longleftrightarrow> Z < 0" definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"