# 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)