Ramana Kumar

It occurs to me that _everything_ can go in `.vim/plugin/sml.vim` (or everything in the `autocmd` but that's more awkward) - perhaps the Vimhol plugin should only be using the former...

Also, for more advanced interaction (with text coming back to vim from HOL) I'd suggest using https://neovim.io and its msgpack-based API to make a better interaction plugin. (This would essentially...

I'm not in favour of making `t1 >- t2` succeed -- I don't think using `THEN1` under a failure-sensitive combinator is an uncommon usage. Perhaps the new parallel `THEN1` could...

`HO_MATCH_MP_TAC test2_ind` won't work in this case because of the paired abstractions. Notice that `HO_MATCH_MP_TAC test1_ind` doesn't work either, but `recInduct` handles the paired abstractions correctly. I guess I'm asking...

In my vision for this, it would also obviate a rebuild in the following situation. `barTheory` depends on `fooTheory`. You add a theorem to `fooTheory` which is not used in...

What happens when there are multiple theorems with the same LHS? Should this trigger a warning or error (if it doesn't already)?

There is a workaround: build the early dependencies with `Holmake` and only use `Holmake --fast` after they are built. This workaround could potentially be automated with a wrapper script. Do...

Actually I think what I mean is not a subgoal cache, but a resulting-goal-state cache keyed on tactic code, to speed up expand (e). This assumes the tactics are pure....

@barakeel would the tactictoe infrastructure support this?

You could try something like: ``` (fn g => subterm (fn tm => Cases_on`^(assert some_condition tm)`) (#2 g) g) ``` where you define `some_condition` to pick out the thing you...