equal
deleted
inserted
replaced
113 lemmas field_bit_defs = |
113 lemmas field_bit_defs = |
114 plus_bit_def times_bit_def minus_bit_def uminus_bit_def |
114 plus_bit_def times_bit_def minus_bit_def uminus_bit_def |
115 divide_bit_def inverse_bit_def |
115 divide_bit_def inverse_bit_def |
116 |
116 |
117 instance |
117 instance |
118 by standard (auto simp: field_bit_defs split: bit.split) |
118 by standard (auto simp: plus_bit_def times_bit_def split: bit.split) |
119 |
119 |
120 end |
120 end |
121 |
121 |
122 lemma bit_add_self: "x + x = 0" for x :: bit |
122 lemma bit_add_self: "x + x = 0" for x :: bit |
123 unfolding plus_bit_def by (simp split: bit.split) |
123 unfolding plus_bit_def by (simp split: bit.split) |