Allow disabling base axioms

[MithicSpirit]

It may be desirable in some cases to prohibit the use of an axiom like "Classical.choice", which goes against constructivity. This could be solved by having a way to prevent isBaseAxiom from working altogether, instead requiring the user to manually tag all the axioms they wish to use. A more elegant solution might be to do something like the unused tactic linter in Mathlib, where an IO.Ref (HashSet _) is used, which can be manually and arbitrarily modified.

[robertylewis]

Thanks for the suggestion. I've added this feature and used it in practice! But I still need to document the validAxioms attribute. See https://github.com/BrownCS1951x/fpv2024/blob/main/LoVe/Homework/Homework2.lean#L114 as an example.