summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/Group.thy

changeset 32960 | 69916a850301 |

parent 31754 | b5260f5272a4 |

child 32989 | c28279b29ff1 |

1.1 --- a/src/HOL/Algebra/Group.thy Sat Oct 17 01:05:59 2009 +0200 1.2 +++ b/src/HOL/Algebra/Group.thy Sat Oct 17 14:43:18 2009 +0200 1.3 @@ -785,16 +785,16 @@ 1.4 assume H: "H \<in> A" 1.5 with L have subgroupH: "subgroup H G" by auto 1.6 from subgroupH have groupH: "group (G (| carrier := H |))" (is "group ?H") 1.7 - by (rule subgroup_imp_group) 1.8 + by (rule subgroup_imp_group) 1.9 from groupH have monoidH: "monoid ?H" 1.10 - by (rule group.is_monoid) 1.11 + by (rule group.is_monoid) 1.12 from H have Int_subset: "?Int \<subseteq> H" by fastsimp 1.13 then show "le ?L ?Int H" by simp 1.14 next 1.15 fix H 1.16 assume H: "H \<in> Lower ?L A" 1.17 with L Int_subgroup show "le ?L H ?Int" 1.18 - by (fastsimp simp: Lower_def intro: Inter_greatest) 1.19 + by (fastsimp simp: Lower_def intro: Inter_greatest) 1.20 next 1.21 show "A \<subseteq> carrier ?L" by (rule L) 1.22 next