src/HOL/Word/Num_Lemmas.thy
changeset 30445 757ba2bb2b39
parent 30242 aea5d7fa7ef5
child 30943 eb3dbbe971f6
equal deleted inserted replaced
30444:62139eb64bfe 30445:757ba2bb2b39
     9 begin
     9 begin
    10 
    10 
    11 lemma contentsI: "y = {x} ==> contents y = x" 
    11 lemma contentsI: "y = {x} ==> contents y = x" 
    12   unfolding contents_def by auto -- {* FIXME move *}
    12   unfolding contents_def by auto -- {* FIXME move *}
    13 
    13 
    14 lemmas split_split = prod.split [unfolded prod_case_split] 
    14 lemmas split_split = prod.split [unfolded prod_case_split]
    15 lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
    15 lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
    16 lemmas "split.splits" = split_split split_split_asm 
    16 lemmas split_splits = split_split split_split_asm
    17 
    17 
    18 lemmas funpow_0 = funpow.simps(1)
    18 lemmas funpow_0 = funpow.simps(1)
    19 lemmas funpow_Suc = funpow.simps(2)
    19 lemmas funpow_Suc = funpow.simps(2)
    20 
    20 
    21 lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto
    21 lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto