src/HOL/Library/Char_nat.thy
changeset 30224 79136ce06bdb
parent 28562 4e74209f113e
child 30663 0b6aff7451b2
     1.1 --- a/src/HOL/Library/Char_nat.thy	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/src/HOL/Library/Char_nat.thy	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4  lemma Char_char_of_nat:
     1.5    "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
     1.6    unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
     1.7 -  by (auto simp add: div_add1_eq mod_add1_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
     1.8 +  by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
     1.9  
    1.10  lemma char_of_nat_of_char:
    1.11    "char_of_nat (nat_of_char c) = c"
    1.12 @@ -165,7 +165,7 @@
    1.13    show ?thesis
    1.14      by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
    1.15        nat_of_nibble_of_nat mod_mult_distrib
    1.16 -      n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
    1.17 +      n aux3 mod_mult_self3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
    1.18  qed
    1.19  
    1.20  lemma nibble_pair_of_nat_char: