equal
deleted
inserted
replaced
167 lemma [code_unfold del]: |
167 lemma [code_unfold del]: |
168 "numeral k \<equiv> (of_rat (numeral k) :: real)" |
168 "numeral k \<equiv> (of_rat (numeral k) :: real)" |
169 by simp |
169 by simp |
170 |
170 |
171 lemma [code_unfold del]: |
171 lemma [code_unfold del]: |
172 "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)" |
172 "- numeral k \<equiv> (of_rat (- numeral k) :: real)" |
173 by simp |
173 by simp |
174 |
174 |
175 hide_const (open) real_of_int |
175 hide_const (open) real_of_int |
176 |
176 |
177 code_printing |
177 code_printing |