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

src/HOL/Algebra/Group.thy

changeset 32960 | 69916a850301 |

parent 31754 | b5260f5272a4 |

child 32989 | c28279b29ff1 |

--- a/src/HOL/Algebra/Group.thy Sat Oct 17 01:05:59 2009 +0200 +++ b/src/HOL/Algebra/Group.thy Sat Oct 17 14:43:18 2009 +0200 @@ -785,16 +785,16 @@ assume H: "H \<in> A" with L have subgroupH: "subgroup H G" by auto from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") - by (rule subgroup_imp_group) + by (rule subgroup_imp_group) from groupH have monoidH: "monoid ?H" - by (rule group.is_monoid) + by (rule group.is_monoid) from H have Int_subset: "?Int \<subseteq> H" by fastsimp then show "le ?L ?Int H" by simp next fix H assume H: "H \<in> Lower ?L A" with L Int_subgroup show "le ?L H ?Int" - by (fastsimp simp: Lower_def intro: Inter_greatest) + by (fastsimp simp: Lower_def intro: Inter_greatest) next show "A \<subseteq> carrier ?L" by (rule L) next