src/HOL/Word/Word.thy
changeset 61424 c3658c18b7bc
parent 61260 e6f03fae14d5
child 61649 268d88ec9087
     1.1 --- a/src/HOL/Word/Word.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -3836,7 +3836,7 @@
     1.4  lemma word_rsplit_empty_iff_size:
     1.5    "(word_rsplit w = []) = (size w = 0)" 
     1.6    unfolding word_rsplit_def bin_rsplit_def word_size
     1.7 -  by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
     1.8 +  by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
     1.9  
    1.10  lemma test_bit_rsplit:
    1.11    "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow>