[isabelle] [symmetric]-attribute changes variable names



Hi all,

I recently stumbled over the following quite confusing behaviour:

definition "foo x \<equiv> x"
thm foo_def[symmetric]
  > Outputs ?y = foo ?y

Is it really necessary that symmetric is allowed to change variable
names in the theorem? For a user, it may be quite confusing having to
write
  foo[where x="bar"], but foo[symmetric, where y="bar"]


-- Peter







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