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
Pure.symmetric.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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