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



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.