equal
deleted
inserted
replaced
43 foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0" |
43 foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0" |
44 by (simp add: of_char_def ac_simps) |
44 by (simp add: of_char_def ac_simps) |
45 |
45 |
46 end |
46 end |
47 |
47 |
48 context semiring_parity |
48 context unique_euclidean_semiring_with_nat |
49 begin |
49 begin |
50 |
50 |
51 definition char_of :: "'a \<Rightarrow> char" |
51 definition char_of :: "'a \<Rightarrow> char" |
52 where "char_of n = Char (odd n) (odd (drop_bit 1 n)) |
52 where "char_of n = Char (odd n) (odd (drop_bit 1 n)) |
53 (odd (drop_bit 2 n)) (odd (drop_bit 3 n)) |
53 (odd (drop_bit 2 n)) (odd (drop_bit 3 n)) |