# [isabelle] 'symmetric' and full proofs

Hello all,
I see that the 'symmetric' option is quite commonly use -- what does
it actually do? For example, from LocaleTest.thy:
lemma rcancel:
"y ** x = z ** x <-> y = z"
proof
assume "y ** x = z ** x"
then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
by (simp add: assoc [symmetric])
then show "y = z" by (simp add: rone rinv)
qed simp
Is it the same as the 'symmetric' that is often found in the output of
full_prf? Are 'combination', 'reflexive', 'transitive', etc. in full
proofs rules like 'exI'? What do these do/mean?
Best,
John

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*