Michael Norrish

Yeah, I wondered if this was another "straying from the Basis".

Certainly, that'd make life here much easier (aiming to make a Windows version of HOL).

I believe this is correct, though weird. NONE represents the local time-zone, as per http://mlton.org/basis/date.html

The exception is raised by `Defn.stdrec_defn`

I assume this would be intended to benefit interactive sessions. It seems like it would be pretty easy to store every theorem statement in a term-net that could be consulted...

Ha! That's good to know. I will check that I can reproduce this problem with Isabelle's `Future` module, and then start prepping for bad uses of references in the metis...

The problem does indeed arise when using the Isabelle concurrency library (which is not so surprising).

There is a problem with making `THEN1` evaluate in parallel. Basically, when we write `t1 >- t2` we want `t2` to evaluate in parallel with the `t3` we imagine will...

Please let me know if you can think of a way to make execution of `t2` happen in parallel with tactics coming later, while still keeping `t1 >- t2` having...

I expect that the non-nested occurrences greatly outnumber the nested ones, meaning that one would have to change fewer things to get the benefit of concurrency in existing code bases.