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
>   safe!
> 
>   It would be helpful if someone can link a document
>   on the command declare.
> 
> 
>   Best,
> 
>   Yakoub.
> 






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