equal
deleted
inserted
replaced
39 |
39 |
40 fun times_rat_raw where |
40 fun times_rat_raw where |
41 "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)" |
41 "times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)" |
42 |
42 |
43 quotient_definition |
43 quotient_definition |
44 "(( * )) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute) |
44 "((*)) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult.assoc mult.left_commute) |
45 |
45 |
46 fun plus_rat_raw where |
46 fun plus_rat_raw where |
47 "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)" |
47 "plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)" |
48 |
48 |
49 quotient_definition |
49 quotient_definition |