theory Groups imports FOL begin locale group = fixes f :: "'a \ 'a \ 'a" (infixl "*" 70) fixes e :: 'a ("1") fixes inv :: "'a \ 'a" ("(_^-1)" [79] 80) assumes assoc : "a * b * c = a * (b * c)" assumes rneutr: "a * 1 = a" assumes rinv: "a * a^-1 = 1" begin (* This does not work as expected in jedit notation inv ("(_\)" [79] 80) *) lemmas assoc_context = subst_context[OF assoc] and rneutr_context = subst_context[OF rneutr] and rinv_context = subst_context[OF rinv] lemmas assoc_context_sym = assoc_context[symmetric] and rneutr_context_sym = rneutr_context[symmetric] and rinv_context_sym = rinv_context[symmetric] end end