[isabelle] [iff] Attribute

Hi there,

do I understand correctly that a lemma declared as [iff] is added as simplification rule (from left to right) as well as intro/elim rule?

What happens with equations? What kind of intro/elim rules do I get from a lemma "A = B". More importantly, is it safe to declare a rule as [iff] (e.g., if I had two different characterizations of A, namely B and C, would it be safe to add [iff]: "A = B" and [iff]: "A = C" or does it depend on the weather afterwards, whether automation does still what I want)?

best regards


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