Michael Norrish

I’ll give it a go.

I've made what I think is the appropriate update to the definition of `float_mul_add`. Is there an analogous update that should be made to `float_mul_sub`? I've included your test-case from...

Absolutely. Of course, if the "alternative" were pursued, not all superscripts would have to be made non-aggregating, and the numeral superscripts would have to stay as they are. We would...

On 6/09/11 5:08 PM, xrchz wrote: > When? By the simplifier? Yeah; in srw_ss() with an appropriate conversion.

Better yet (perhaps?): detect if FS is case-insensitive, record this fact, and then change operations like `load` to normalise filenames before using then.

The flagging of theorems, whether white-listing (with associated categories?) or marking as interesting could obviously be done with theorem attributes.

Yeah, I think you're right.

Don't know how keen I am on this when existing monad syntax would also work. For example ```` [ x + 1 | x

I think the syntax here should use a string argument, and that the string should then be encoded into the “using assumption”. (One might imagine changing the type of tactics...

As you say, `ho_match_mp_tac` doesn't do all that `Induct_on` does. And in fact, I want `Induct_on` to do still more. For example, when working with `FINITE_INDUCT`, have it cope with...