summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_examples/Group.thy

changeset 7005 | cc778d613217 |

parent 6908 | 1bf0590f4790 |

child 7133 | 64c9f2364dae |

equal
deleted
inserted
replaced

7004:c799d0859638 | 7005:cc778d613217 |
---|---|

126 monoid_assoc: "(x * y) * z = x * (y * z)" |
126 monoid_assoc: "(x * y) * z = x * (y * z)" |

127 monoid_left_unit: "one * x = x" |
127 monoid_left_unit: "one * x = x" |

128 monoid_right_unit: "x * one = x"; |
128 monoid_right_unit: "x * one = x"; |

129 |
129 |

130 text {* |
130 text {* |

131 Groups are *not* yet monoids directly from the definition . For |
131 Groups are *not* yet monoids directly from the definition. For |

132 monoids, right_unit had to be included as an axiom, but for groups |
132 monoids, right_unit had to be included as an axiom, but for groups |

133 both right_unit and right_inverse are derivable from the other |
133 both right_unit and right_inverse are derivable from the other |

134 axioms. With group_right_unit derived as a theorem of group theory |
134 axioms. With group_right_unit derived as a theorem of group theory |

135 (see above), we may still instantiate group < monoid properly as |
135 (see above), we may still instantiate group < monoid properly as |

136 follows. |
136 follows. |