src/HOL/String.thy
changeset 63950 cdc1e59aa513
parent 62678 843ff6f1de38
child 64630 96015aecfeba
     1.1 --- a/src/HOL/String.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/String.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4  lemma integer_of_char_Char [simp]:
     1.5    "integer_of_char (Char k) = numeral k mod 256"
     1.6    by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
     1.7 -    id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
     1.8 +    id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
     1.9  
    1.10  lemma less_256_integer_of_char_Char:
    1.11    assumes "numeral k < (256 :: integer)"