# HG changeset patch # User wenzelm # Date 1236796024 -3600 # Node ID 757ba2bb2b3973c52c3051255233cdbb7eed9499 # Parent 62139eb64bfe54fa9fbead7ce4a240a9d83b892a renamed (unused?) "split.splits" to split_splits -- it was only accepted by accident; diff -r 62139eb64bfe -r 757ba2bb2b39 src/HOL/Word/Num_Lemmas.thy --- a/src/HOL/Word/Num_Lemmas.thy Wed Mar 11 17:51:01 2009 +0100 +++ b/src/HOL/Word/Num_Lemmas.thy Wed Mar 11 19:27:04 2009 +0100 @@ -11,9 +11,9 @@ lemma contentsI: "y = {x} ==> contents y = x" unfolding contents_def by auto -- {* FIXME move *} -lemmas split_split = prod.split [unfolded prod_case_split] +lemmas split_split = prod.split [unfolded prod_case_split] lemmas split_split_asm = prod.split_asm [unfolded prod_case_split] -lemmas "split.splits" = split_split split_split_asm +lemmas split_splits = split_split split_split_asm lemmas funpow_0 = funpow.simps(1) lemmas funpow_Suc = funpow.simps(2)