Re: [isabelle] Using declare to remove rules from auto and safe
Depends if it is a simp rule or a logic rule:
For logic rules:
declare exI[rule del]
For simp rules use:
declare fun_eq_iff[simp del]
Am Mittwoch, den 28.10.2015, 13:58 +0100 schrieb nemouchi:
> Hi all,
> I want to remove some rules that auto and safe use on proof context.
> Is it possible to use declare and remove a given rule from the set of
> rules inside auto and safe?
> If yes, can someone give me an example on how can we do that (the
> options that declare needs) ? example removing a given rule used by
> It would be helpful if someone can link a document
> on the command declare.
This archive was generated by a fusion of
Pipermail (Mailman edition) and