equal
deleted
inserted
replaced
370 by (simp add: Dedekind_Real.cut_def) |
370 by (simp add: Dedekind_Real.cut_def) |
371 qed |
371 qed |
372 |
372 |
373 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)" |
373 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)" |
374 apply (simp add: preal_mult_def mem_mult_set Rep_preal) |
374 apply (simp add: preal_mult_def mem_mult_set Rep_preal) |
375 apply (force simp: mult_set_def ac_simps) |
375 apply (simp add: mult_set_def) |
|
376 apply (metis (no_types, hide_lams) ab_semigroup_mult_class.mult_ac(1)) |
376 done |
377 done |
377 |
378 |
378 instance preal :: ab_semigroup_mult |
379 instance preal :: ab_semigroup_mult |
379 proof |
380 proof |
380 fix a b c :: preal |
381 fix a b c :: preal |