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