case bash tactic

Stream: general

[Johan Commelin]

@Scott Morrison I incorrectly assumed that your case_bash tactic was related to the fin-bashing tactic. Nevertheless I wonder if there is place for a mechanism as follows:

• case_bash goes into tactics/
• tidy takes an optional list of tactics to apply (besides the local [attribute] thing that we use nowadays)
• So we can prove thing with tidy [case_bash] or something like that.

Does that make sense?

[Scott Morrison]

I think you can already override the list of tactics: tidy { tactics := tactic.tidy.default_tactics ++ [foo] }, although foo has to be a tactic string for this to work.

[Scott Morrison]

Certainly that can be given nicer syntax, and use some reflection to allow passing more complicated things than just a tactic string.

[Scott Morrison]

(e.g. a tactic A for any A, a function with arguments that have default values, etc.)