Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Using declare to remove rules from auto and safe

view this post on Zulip Email Gateway (Aug 22 2022 at 11:38):

From: nemouchi <Yakoub.Nemouchi@lri.fr>
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.

view this post on Zulip Email Gateway (Aug 22 2022 at 11:38):

From: Johannes Hölzl <hoelzl@in.tum.de>
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]

Last updated: Apr 25 2024 at 12:23 UTC