Re: [isabelle] 'symmetric' and full proofs

Hi John,

> I see. Do you know where 'symmetric' is defined? Also, how about 'combination'?

just to avoid confusion: symmetric and combination as appearing in proof
terms are rules (axioms) of the logical framework;  symmetric also
appears as theorem in theory Pure:

thm Pure.symmetric

These rules are implemented in the inference kernel of the system and
not defined in an Isar theory.

Distinguish from these the attribute "symmetric", which may apply one
rule of a larger set of symmetry theorems, one of these being

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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