src/HOL/String.thy
changeset 57512 cc97b347b301
parent 57437 0baf08c075b9
child 58152 6fe60a9a5bad
     1.1 --- a/src/HOL/String.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/String.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -269,7 +269,7 @@
     1.4  lemma nibble_of_nat_of_char_div_16:
     1.5    "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
     1.6    by (cases c)
     1.7 -    (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
     1.8 +    (simp add: nat_of_char_def add.commute nat_of_nibble_less_16)
     1.9  
    1.10  lemma nibble_of_nat_nat_of_char:
    1.11    "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
    1.12 @@ -279,7 +279,7 @@
    1.13      by (simp add: nibble_of_nat_mod_16)
    1.14    then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
    1.15      by (simp only: nibble_of_nat_mod_16)
    1.16 -  with Char show ?thesis by (simp add: nat_of_char_def add_commute)
    1.17 +  with Char show ?thesis by (simp add: nat_of_char_def add.commute)
    1.18  qed
    1.19  
    1.20  code_datatype Char -- {* drop case certificate for char *}
    1.21 @@ -303,7 +303,7 @@
    1.22    have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
    1.23    then show ?thesis
    1.24      by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
    1.25 -      card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
    1.26 +      card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add.commute)
    1.27  qed
    1.28  
    1.29  lemma char_of_nat_of_char [simp]: