src/HOL/Algebra/Group.thy
changeset 63167 0909deb8059b
parent 61628 8dd2bd4fe30b
child 65099 30d0b2f1df76
     1.1 --- a/src/HOL/Algebra/Group.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  definition
     1.6    Units :: "_ => 'a set"
     1.7 -  --\<open>The set of invertible elements\<close>
     1.8 +  \<comment>\<open>The set of invertible elements\<close>
     1.9    where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
    1.10  
    1.11  consts
    1.12 @@ -98,7 +98,7 @@
    1.13    moreover from x y xinv yinv have "x \<otimes> (y \<otimes> y') \<otimes> x' = \<one>" by simp
    1.14    moreover note x y
    1.15    ultimately show ?thesis unfolding Units_def
    1.16 -    -- "Must avoid premature use of @{text hyp_subst_tac}."
    1.17 +    \<comment> "Must avoid premature use of \<open>hyp_subst_tac\<close>."
    1.18      apply (rule_tac CollectI)
    1.19      apply (rule)
    1.20      apply (fast)
    1.21 @@ -486,8 +486,8 @@
    1.22  
    1.23  text \<open>
    1.24    Since @{term H} is nonempty, it contains some element @{term x}.  Since
    1.25 -  it is closed under inverse, it contains @{text "inv x"}.  Since
    1.26 -  it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
    1.27 +  it is closed under inverse, it contains \<open>inv x\<close>.  Since
    1.28 +  it is closed under product, it contains \<open>x \<otimes> inv x = \<one>\<close>.
    1.29  \<close>
    1.30  
    1.31  lemma (in group) one_in_subset: