Michael Norrish

You stash the name of the theorem, encoded as variable (using, `K T name` say).

Work on this has been happening in 436637988 and e99f87f3816.

Needs documenting, but I think this is basically done.

Sounds great!

Strictly speaking, the theorem is not entirely useless and is treated as ``` P a b ==> ((f a = g b) T) ```

If something like this was to be implemented, one approach would be to do what is the equivalent of a `drule` or `IMP_RES_THEN` as the rewrites were being normalised and...

This would be a nice project for sure! Having heard so much about the Intel work I just assumed that all the chips supported these functions in hardware (in which...

The followup would be to have the parser do the same. It seems as if the logic could model the stream as a lazy list, but have compilation magically treat...

Certainly, the `LUNFOLD` function connects a state-monad function to a lazy list...

I generated something along these lines when I generated the dependency graphs; I think it's a pretty easy change to the existing `DOT` script in HOL. I'm not sure that...