[isabelle] Using declare to remove rules from auto and safe
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Using declare to remove rules from auto and safe
- From: nemouchi <Yakoub.Nemouchi at lri.fr>
- Date: Wed, 28 Oct 2015 13:58:17 +0100
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: LRI Webmail/0.9.5
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