Thomas Tuerk

I played around with this a bit. I can confirm this behavior, but only at the end of a file. If the tactic is followed by "THEN", ">>", "val" and...

I believe the new simple quantifier heuristics, in particular `SIMPLE_SOME_INSTANTIATE_CONV` implement this.

@tanyongkiam I of course don't know your exact situation, but this kind of case split on the first matched pattern was part of the motivation behind having a different representation...

Something like this is implemented in the quantifier heuristics lib. There is no fast, special purpose conversion, though. ```` > SIMP_CONV (std_ss++QI_ss) [] ``!xyz. P ((\(aa, cc, bb). f aa...

There is now better support for creating equations. This also helps with the function definitions issues, but more work is needed there. If you are interested, read the new Section...

Hi, not sure whether this is useful, but HOL's pattern compilation implementation in _src/1/Pmatch_ is using ideas from "Compiling Pattern Matching to Good Decisions Trees". Perhaps one can salvage some...