Loading theory "Secondary_Sylow.GroupAction" (required by "Jordan_Hoelder.JordanHolder" via "Jordan_Hoelder.CompositionSeries" via "Jordan_Hoelder.SimpleGroups" via "Jordan_Hoelder.SubgroupsAndNormalSubgroups" via "Secondary_Sylow.SndSylow" via "Secondary_Sylow.SubgroupConjugation")
Loading theory "Jordan_Hoelder.GroupIsoClasses" (required by "Jordan_Hoelder.JordanHolder")
### No map function defined for GroupIsoClasses.group. This will cause problems later on.
### Generation of a parametrized correspondence relation failed.
### Reason:  No relator for the type "GroupIsoClasses.group" found.
### theory "Jordan_Hoelder.GroupIsoClasses"
### 0.265s elapsed time, 0.620s cpu time, 0.000s GC time
locale group_action
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
    and \<phi> :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and M :: "'c set"
  assumes "group_action G \<phi> M"
locale group_action
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
    and \<phi> :: "'a \<Rightarrow> 'c \<Rightarrow> 'c"
    and M :: "'c set"
  assumes "group_action G \<phi> M"
### theory "Secondary_Sylow.GroupAction"
### 0.717s elapsed time, 1.488s cpu time, 0.000s GC time
Loading theory "Secondary_Sylow.SubgroupConjugation" (required by "Jordan_Hoelder.JordanHolder" via "Jordan_Hoelder.CompositionSeries" via "Jordan_Hoelder.SimpleGroups" via "Jordan_Hoelder.SubgroupsAndNormalSubgroups" via "Secondary_Sylow.SndSylow")
locale Group.group
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
  assumes "Group.group G"
### Ambiguous input (line 41 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" H))
###     ("_position" H)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" H))
###     ("_position" H)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 69 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" card)
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("_position" M)))
###     ("_applC" ("_position" card) ("_position" M))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" card)
###       ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" M)))
###     ("_applC" ("_position" card) ("_position" M))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 106 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" subgroup)
###     ("_cargs"
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" H) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g))))
###       ("_position" G))))
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" subgroup)
###     ("_cargs"
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" H) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g))))
###       ("_position" G))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 156 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" conjugation_action) ("_position" p))
###     ("_lam" ("_position" g) ("_applC" ("_position" carrier) ("_position" G))
###       ("_lam" ("_position" P)
###         ("_applC" ("_position" subgroups_of_size) ("_position" p))
###         ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" conjugation_action) ("_position" p))
###     ("_lam" ("_position" g) ("_applC" ("_position" carrier) ("_position" G))
###       ("_lam" ("_position" P)
###         ("_applC" ("_position" subgroups_of_size) ("_position" p))
###         ("\<^const>Multiset.subset_mset" ("_position" g)
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 237 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###         ("_position" h)))
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("_position" P))
###       ("_indexdefault") ("_position" h))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###         ("_position" h)))
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("_position" P))
###       ("_indexdefault") ("_position" h))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###         ("_position" h)))
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" P))
###       ("_indexdefault") ("_position" h))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###         ("_position" h)))
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" P))
###       ("_indexdefault") ("_position" h))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 349 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("_position" P)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("_position" P)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "Secondary_Sylow.SubgroupConjugation"
### 0.227s elapsed time, 0.452s cpu time, 0.000s GC time
Loading theory "Secondary_Sylow.SndSylow" (required by "Jordan_Hoelder.JordanHolder" via "Jordan_Hoelder.CompositionSeries" via "Jordan_Hoelder.SimpleGroups" via "Jordan_Hoelder.SubgroupsAndNormalSubgroups")
Loading theory "Jordan_Hoelder.SndIsomorphismGrp" (required by "Jordan_Hoelder.JordanHolder" via "Jordan_Hoelder.CompositionSeries" via "Jordan_Hoelder.SimpleGroups" via "Jordan_Hoelder.SubgroupsAndNormalSubgroups")
locale second_isomorphism_grp
  fixes H :: "'a set"
    and G :: "('a, 'b) monoid_scheme"  (structure)
    and S :: "'a set"
  assumes "second_isomorphism_grp H G S"
locale second_isomorphism_grp
  fixes H :: "'a set"
    and G :: "('a, 'b) monoid_scheme"  (structure)
    and S :: "'a set"
  assumes "second_isomorphism_grp H G S"
### theory "Jordan_Hoelder.SndIsomorphismGrp"
### 0.242s elapsed time, 0.480s cpu time, 0.000s GC time
locale Group.group
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
  assumes "Group.group G"
locale snd_sylow
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
    and p :: "nat"
    and a :: "nat"
    and m :: "nat"
    and calM :: "'a set set"
    and RelM :: "('a set \<times> 'a set) set"
  assumes "snd_sylow G p a m"
  defines "calM \<equiv> {s. s \<subseteq> carrier G \<and> card s = p ^ a}"
    and
    "RelM \<equiv>
     {(N1, N2).
      N1 \<in> calM \<and>
      N2 \<in> calM \<and> (\<exists>g\<in>carrier G. N1 = N2 #> g)}"
locale snd_sylow
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
    and p :: "nat"
    and a :: "nat"
    and m :: "nat"
    and calM :: "'a set set"
    and RelM :: "('a set \<times> 'a set) set"
  assumes "snd_sylow G p a m"
  defines "calM \<equiv> {s. s \<subseteq> carrier G \<and> card s = p ^ a}"
    and
    "RelM \<equiv>
     {(N1, N2).
      N1 \<in> calM \<and>
      N2 \<in> calM \<and> (\<exists>g\<in>carrier G. N1 = N2 #> g)}"
### theory "Secondary_Sylow.SndSylow"
### 0.805s elapsed time, 1.536s cpu time, 0.348s GC time
Loading theory "Jordan_Hoelder.SubgroupsAndNormalSubgroups" (required by "Jordan_Hoelder.JordanHolder" via "Jordan_Hoelder.CompositionSeries" via "Jordan_Hoelder.SimpleGroups")
### Ambiguous input (line 226 of "$AFP/Jordan_Hoelder/SubgroupsAndNormalSubgroups.thy") produces 2 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.subset_eq" ("_position" H)
###         ("_applC" ("_position" carrier) ("_position" G))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.subset_eq" ("_position" K)
###           ("_applC" ("_position" carrier) ("_position" G))))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.member" ("_position" x)
###             ("_applC" ("_position" carrier) ("_position" G)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Coset.set_mult_indexed"
###         ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###           ("_position" H))
###         ("_indexdefault") ("_position" K))
###       ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###         ("\<^const>Coset.set_mult_indexed" ("_position" H) ("_indexdefault")
###           ("_position" K))))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>Set.subset_eq" ("_position" H)
###         ("_applC" ("_position" carrier) ("_position" G))))
###     ("_asms"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>Set.subset_eq" ("_position" K)
###           ("_applC" ("_position" carrier) ("_position" G))))
###       ("_asm"
###         ("\<^const>HOL.Trueprop"
###           ("\<^const>Set.member" ("_position" x)
###             ("_applC" ("_position" carrier) ("_position" G)))))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>HOL.eq"
###       ("\<^const>Coset.set_mult_indexed"
###         ("\<^const>Multiset.subset_mset" ("_position" x) ("_position" H))
###         ("_indexdefault") ("_position" K))
###       ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###         ("\<^const>Coset.set_mult_indexed" ("_position" H) ("_indexdefault")
###           ("_position" K))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "Jordan_Hoelder.SubgroupsAndNormalSubgroups"
### 0.498s elapsed time, 1.000s cpu time, 0.000s GC time
Loading theory "Jordan_Hoelder.SimpleGroups" (required by "Jordan_Hoelder.JordanHolder" via "Jordan_Hoelder.CompositionSeries")
locale simple_group
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
  assumes "simple_group G"
### theory "Jordan_Hoelder.SimpleGroups"
### 0.110s elapsed time, 0.220s cpu time, 0.000s GC time
Loading theory "Jordan_Hoelder.MaximalNormalSubgroups" (required by "Jordan_Hoelder.JordanHolder" via "Jordan_Hoelder.CompositionSeries")
locale max_normal_subgroup
  fixes H :: "'a set"
    and G :: "('a, 'b) monoid_scheme"  (structure)
  assumes "max_normal_subgroup H G"
### theory "Jordan_Hoelder.MaximalNormalSubgroups"
### 0.084s elapsed time, 0.168s cpu time, 0.000s GC time
Loading theory "Jordan_Hoelder.CompositionSeries" (required by "Jordan_Hoelder.JordanHolder")
locale normal_series
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
    and \<GG> :: "'a set list"
  assumes "normal_series G \<GG>"
locale composition_series
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
    and \<GG> :: "'a set list"
  assumes "composition_series G \<GG>"
### Ignoring duplicate rewrite rule:
### hd (remdups_adj ?xs1) \<equiv> hd ?xs1
### theory "Jordan_Hoelder.CompositionSeries"
### 0.593s elapsed time, 1.188s cpu time, 0.000s GC time
Loading theory "Jordan_Hoelder.JordanHolder"
locale jordan_hoelder
  fixes G :: "('a, 'b) monoid_scheme"  (structure)
    and \<HH> :: "'a set list"
    and \<GG> :: "'a set list"
  assumes "jordan_hoelder G \<HH> \<GG>"
### theory "Jordan_Hoelder.JordanHolder"
### 0.443s elapsed time, 0.880s cpu time, 0.000s GC time
### Ambiguous input (line 71 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" bij_betw)
###     ("_cargs"
###       ("_lambda" ("_position" m)
###         ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###           ("_indexdefault") ("_position" m)))
###       ("_cargs" ("_position" M)
###         ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###           ("_position" M))))))
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" bij_betw)
###     ("_cargs"
###       ("_lambda" ("_position" m)
###         ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###           ("_indexdefault") ("_position" m)))
###       ("_cargs" ("_position" M)
###         ("\<^const>Multiset.subset_mset" ("_position" g)
###           ("_position" M))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 94 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" card)
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("_position" M)))
###     ("_applC" ("_position" card) ("_position" M))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" card)
###       ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" M)))
###     ("_applC" ("_position" card) ("_position" M))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 170 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" subgroup)
###     ("_cargs"
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g))))
###       ("_position" G))))
### ("\<^const>HOL.Trueprop"
###   ("_applC" ("_position" subgroup)
###     ("_cargs"
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g))))
###       ("_position" G))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 173 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" card)
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("_position" p)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" card)
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("_position" p)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 244 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member" ("_position" x)
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("_position" P))
###       ("_indexdefault") ("_position" h))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member" ("_position" x)
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" P))
###       ("_indexdefault") ("_position" h))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 247 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member" ("_position" x)
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("_position" P))
###       ("_indexdefault") ("_position" h))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member" ("_position" x)
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" P))
###       ("_indexdefault") ("_position" h))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 194 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" g))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" g))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 195 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 8 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Multiset.subset_mset" ("_position" g)
###         ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" g)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 196 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.mult_indexed"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.mult_indexed"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" g))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.monoid.mult_indexed"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("_indexdefault") ("_position" g))
###       ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.mult_indexed"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" g))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 197 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.one_indexed" ("_indexdefault"))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.one_indexed" ("_indexdefault"))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" g))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.monoid.one_indexed" ("_indexdefault"))
###       ("\<^const>Coset.r_coset_indexed" ("_position" U) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.one_indexed" ("_indexdefault"))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" V) ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" g))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 277 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("_lam" ("_position" P)
###       ("_applC" ("_position" subgroups_of_size) ("_position" p))
###       ("\<^const>Multiset.subset_mset"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###               ("_indexdefault") ("_position" y))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("_lam" ("_position" P)
###       ("_applC" ("_position" subgroups_of_size) ("_position" p))
###       ("\<^const>Coset.l_coset_indexed"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))
###         ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###               ("_indexdefault") ("_position" y))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 286 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" conjx)
###       ("_applC" ("_position" conjy) ("_position" P)))
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Multiset.subset_mset" ("_position" y)
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" y))))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC" ("_position" conjx)
###       ("_applC" ("_position" conjy) ("_position" P)))
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.l_coset_indexed" ("_position" y) ("_indexdefault")
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" y))))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" x))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 287 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.r_coset_indexed"
###           ("\<^const>Coset.l_coset_indexed" ("_position" y)
###             ("_indexdefault") ("_position" P))
###           ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" y)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" x))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.r_coset_indexed"
###           ("\<^const>Multiset.subset_mset" ("_position" y) ("_position" P))
###           ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" y)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("_position" x))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 288 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Multiset.subset_mset" ("_position" y) ("_position" P))
###         ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" y))
###           ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" x)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.l_coset_indexed" ("_position" y) ("_indexdefault")
###           ("_position" P))
###         ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" y))
###           ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("_position" x)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 289 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Multiset.subset_mset" ("_position" y) ("_position" P))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###             ("_indexdefault") ("_position" y)))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.l_coset_indexed" ("_position" y) ("_indexdefault")
###           ("_position" P))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###           ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###             ("_indexdefault") ("_position" y)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 214 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Multiset.subset_mset"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_UNION" ("_position" p) ("_position" P)
###       ("_Finset"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###           ("_indexdefault")
###           ("\<^const>Group.monoid.mult_indexed"
###             ("\<^const>Group.monoid.mult_indexed"
###               ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###                 ("_position" g))
###               ("_indexdefault")
###               ("\<^const>Group.monoid.mult_indexed" ("_position" p)
###                 ("_indexdefault") ("_position" g)))
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Multiset.subset_mset"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_UNION" ("_position" p) ("_position" P)
###       ("_Finset"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###           ("_indexdefault")
###           ("\<^const>Group.monoid.mult_indexed"
###             ("\<^const>Group.monoid.mult_indexed"
###               ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###                 ("_position" g))
###               ("_indexdefault")
###               ("\<^const>Group.monoid.mult_indexed" ("_position" p)
###                 ("_indexdefault") ("_position" g)))
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.l_coset_indexed"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("_indexdefault")
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_UNION" ("_position" p) ("_position" P)
###       ("_Finset"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###           ("_indexdefault")
###           ("\<^const>Group.monoid.mult_indexed"
###             ("\<^const>Group.monoid.mult_indexed"
###               ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###                 ("_position" g))
###               ("_indexdefault")
###               ("\<^const>Group.monoid.mult_indexed" ("_position" p)
###                 ("_indexdefault") ("_position" g)))
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.l_coset_indexed"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("_indexdefault")
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_UNION" ("_position" p) ("_position" P)
###       ("_Finset"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###           ("_indexdefault")
###           ("\<^const>Group.monoid.mult_indexed"
###             ("\<^const>Group.monoid.mult_indexed"
###               ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###                 ("_position" g))
###               ("_indexdefault")
###               ("\<^const>Group.monoid.mult_indexed" ("_position" p)
###                 ("_indexdefault") ("_position" g)))
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 290 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###         ("\<^const>Multiset.subset_mset" ("_position" y) ("_position" P)))
###       ("_indexdefault")
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Multiset.subset_mset" ("_position" x)
###         ("\<^const>Multiset.subset_mset" ("_position" y) ("_position" P)))
###       ("_indexdefault")
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###         ("\<^const>Coset.l_coset_indexed" ("_position" y) ("_indexdefault")
###           ("_position" P)))
###       ("_indexdefault")
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Multiset.subset_mset" ("_position" x)
###         ("\<^const>Coset.l_coset_indexed" ("_position" y) ("_indexdefault")
###           ("_position" P)))
###       ("_indexdefault")
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 291 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Coset.l_coset_indexed"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))
###         ("_indexdefault") ("_position" P))
###       ("_indexdefault")
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.r_coset_indexed"
###       ("\<^const>Multiset.subset_mset"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))
###         ("_position" P))
###       ("_indexdefault")
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 295 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Group.monoid.mult_indexed" ("_position" conjx)
###       ("_index"
###         ("_applC" ("_position" BijGroup)
###           ("_applC" ("_position" subgroups_of_size) ("_position" p))))
###       ("_position" conjy))
###     ("_lam" ("_position" P)
###       ("_applC" ("_position" subgroups_of_size) ("_position" p))
###       ("\<^const>Multiset.subset_mset"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###               ("_indexdefault") ("_position" y))))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Group.monoid.mult_indexed" ("_position" conjx)
###       ("_index"
###         ("_applC" ("_position" BijGroup)
###           ("_applC" ("_position" subgroups_of_size) ("_position" p))))
###       ("_position" conjy))
###     ("_lam" ("_position" P)
###       ("_applC" ("_position" subgroups_of_size) ("_position" p))
###       ("\<^const>Coset.l_coset_indexed"
###         ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###           ("_indexdefault") ("_position" y))
###         ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" P) ("_indexdefault")
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###             ("\<^const>Group.monoid.mult_indexed" ("_position" x)
###               ("_indexdefault") ("_position" y))))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 226 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Multiset.subset_mset"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_position" P)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Multiset.subset_mset"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_position" P)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.l_coset_indexed"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("_indexdefault")
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_position" P)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.r_coset_indexed"
###         ("\<^const>Coset.l_coset_indexed"
###           ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###           ("_indexdefault")
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault") ("_position" g)))
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))))
###     ("_position" P)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 227 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member" ("_position" P)
###     ("\<^const>Set.image"
###       ("_lambda" ("_position" P)
###         ("\<^const>Multiset.subset_mset" ("_position" g)
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g)))))
###       ("_applC" ("_position" subgroups_of_size) ("_position" p)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member" ("_position" P)
###     ("\<^const>Set.image"
###       ("_lambda" ("_position" P)
###         ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###           ("\<^const>Coset.r_coset_indexed" ("_position" P)
###             ("_indexdefault")
###             ("\<^const>Group.m_inv_indexed" ("_indexdefault")
###               ("_position" g)))))
###       ("_applC" ("_position" subgroups_of_size) ("_position" p)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 353 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 4 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Multiset.subset_mset"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###           ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Multiset.subset_mset"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###           ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###           ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset" ("_position" g)
###       ("\<^const>Coset.l_coset_indexed"
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###         ("_indexdefault")
###         ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###           ("_position" g))))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 354 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g)))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.monoid.mult_indexed" ("_position" g)
###         ("_indexdefault")
###         ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g)))
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 355 of "$AFP/Secondary_Sylow/SubgroupConjugation.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.monoid.one_indexed" ("_indexdefault"))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.monoid.one_indexed" ("_indexdefault"))
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###       ("_position" P))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
*** Failed to refine any pending goal
*** At command "by" (line 171 of "$AFP/Jordan_Hoelder/SndIsomorphismGrp.thy")
### Ambiguous input (line 175 of "$AFP/Jordan_Hoelder/SubgroupsAndNormalSubgroups.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Set.image" ("_position" \<phi>)
###       ("\<^const>Coset.l_coset_indexed" ("_position" g) ("_indexdefault")
###         ("_position" H)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Set.image" ("_position" \<phi>)
###       ("\<^const>Multiset.subset_mset" ("_position" g) ("_position" H)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 243 of "$AFP/Jordan_Hoelder/SubgroupsAndNormalSubgroups.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.set_mult_indexed" ("_position" M) ("_indexdefault")
###       ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###         ("_position" N)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.set_mult_indexed" ("_position" M) ("_indexdefault")
###       ("\<^const>Multiset.subset_mset" ("_position" x) ("_position" N)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 245 of "$AFP/Jordan_Hoelder/SubgroupsAndNormalSubgroups.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.set_mult_indexed"
###       ("\<^const>Coset.l_coset_indexed" ("_position" x) ("_indexdefault")
###         ("_position" M))
###       ("_indexdefault") ("_position" N))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("_DDDOT")
###     ("\<^const>Coset.set_mult_indexed"
###       ("\<^const>Multiset.subset_mset" ("_position" x) ("_position" M))
###       ("_indexdefault") ("_position" N))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 34 of "$AFP/Jordan_Hoelder/CompositionSeries.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Multiset.subset_mset"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("_position" Q)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Coset.l_coset_indexed"
###       ("\<^const>Group.m_inv_indexed" ("_indexdefault") ("_position" g))
###       ("_indexdefault")
###       ("\<^const>Coset.r_coset_indexed" ("_position" Q) ("_indexdefault")
###         ("_position" g)))
###     ("_position" Q)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
*** Failed to finish proof (line 763 of "$AFP/Jordan_Hoelder/CompositionSeries.thy"):
*** goal (1 subgoal):
***  1. \<lbrakk>\<GG> ! Suc i \<inter> K \<lhd> G
***              \<lparr>carrier := \<GG> ! Suc i\<rparr>;
***      \<GG> ! i \<lhd> G\<lparr>carrier := \<GG> ! Suc i\<rparr>;
***      Group.group (G\<lparr>carrier := \<GG> ! Suc i\<rparr>);
***      \<And>G M N.
***         \<lbrakk>Group.group G; M \<lhd> G; N \<lhd> G\<rbrakk>
***         \<Longrightarrow> M <#>\<^bsub>G\<^esub> N \<lhd> G\<rbrakk>
***     \<Longrightarrow> \<GG> ! i <#> \<GG> ! Suc i \<inter> K \<lhd> G
***                       \<lparr>carrier := \<GG> ! Suc i\<rparr>
*** At command "by" (line 763 of "$AFP/Jordan_Hoelder/CompositionSeries.thy")
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jordan_Hoelder/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 763 of "$AFP/Jordan_Hoelder/CompositionSeries.thy"):
*** goal (1 subgoal):
***  1. \<lbrakk>\<GG> ! Suc i \<inter> K \<lhd> G
***              \<lparr>carrier := \<GG> ! Suc i\<rparr>;
***      \<GG> ! i \<lhd> G\<lparr>carrier := \<GG> ! Suc i\<rparr>;
***      Group.group (G\<lparr>carrier := \<GG> ! Suc i\<rparr>);
***      \<And>G M N.
***         \<lbrakk>Group.group G; M \<lhd> G; N \<lhd> G\<rbrakk>
***         \<Longrightarrow> M <#>\<^bsub>G\<^esub> N \<lhd> G\<rbrakk>
***     \<Longrightarrow> \<GG> ! i <#> \<GG> ! Suc i \<inter> K \<lhd> G
***                       \<lparr>carrier := \<GG> ! Suc i\<rparr>
*** At command "by" (line 763 of "$AFP/Jordan_Hoelder/CompositionSeries.thy")
*** Failed to refine any pending goal
*** At command "by" (line 171 of "$AFP/Jordan_Hoelder/SndIsomorphismGrp.thy")