equal
deleted
inserted
replaced
226 show "\<dots> = has_edge (G1 * (G2 * G3)) p J q" |
226 show "\<dots> = has_edge (G1 * (G2 * G3)) p J q" |
227 by (simp only:in_grcomp mult_assoc) blast |
227 by (simp only:in_grcomp mult_assoc) blast |
228 qed |
228 qed |
229 qed |
229 qed |
230 |
230 |
231 instance graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower}" |
231 instance graph :: (type, monoid_mult) "{semiring_1, idem_add}" |
232 proof |
232 proof |
233 fix a b c :: "('a, 'b) graph" |
233 fix a b c :: "('a, 'b) graph" |
234 |
234 |
235 show "1 * a = a" |
235 show "1 * a = a" |
236 by (rule graph_ext) (auto simp:in_grcomp in_grunit) |
236 by (rule graph_ext) (auto simp:in_grcomp in_grunit) |