Re: [isabelle] [iff] Attribute



The attribute [iff] attempts to transform the supplied theorems into introduction and elimination rules sensibly. If the supplied theorem is a non-boolean equality (or other atomic formula), then there is no elimination rule, and the theorem is given the attribute [intro!].
Larry Paulson


On 14 Sep 2010, at 07:17, Christian Sternagel wrote:

> 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
> 
> chris
> 






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