| changeset 39910 | 10097e0a9dbd |
| parent 37887 | 2ae085b07f2f |
| child 44821 | a92f65e174cf |
--- a/src/HOL/Word/Misc_Numeric.thy Fri Oct 01 14:15:49 2010 +0200 +++ b/src/HOL/Word/Misc_Numeric.thy Fri Oct 01 16:05:25 2010 +0200 @@ -8,8 +8,8 @@ imports Main Parity begin -lemma contentsI: "y = {x} ==> contents y = x" - unfolding contents_def by auto -- {* FIXME move *} +lemma the_elemI: "y = {x} ==> the_elem y = x" + by simp lemmas split_split = prod.split lemmas split_split_asm = prod.split_asm