equal
deleted
inserted
replaced
94 lemma number_of_rat [code unfold]: |
94 lemma number_of_rat [code unfold]: |
95 "(number_of k \<Colon> rat) \<equiv> Fract k 1" |
95 "(number_of k \<Colon> rat) \<equiv> Fract k 1" |
96 unfolding Fract_of_int_eq rat_number_of_def by simp |
96 unfolding Fract_of_int_eq rat_number_of_def by simp |
97 |
97 |
98 lemma rat_minus [code func]: |
98 lemma rat_minus [code func]: |
99 "(a\<Colon>rat) - b = a + (- b)" unfolding ab_group_add_class.diff_minus .. |
99 "(a\<Colon>rat) - b = a + (- b)" unfolding diff_minus .. |
100 |
100 |
101 lemma rat_divide [code func]: |
101 lemma rat_divide [code func]: |
102 "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse .. |
102 "(a\<Colon>rat) / b = a * inverse b" unfolding divide_inverse .. |
103 |
103 |
104 instance rat :: eq .. |
104 instance rat :: eq .. |