Poly/ML

[Stephen Weeks]

> I did a scan of their (Poly/ML) web page and it seems that Paulson wasn't
> involved in writing it, but he was one of the first users, so he probably had
> a lot of influence on what got optimized.

Sorry, I meant to say Matthews is the main (only?) author.

> I'm quite confused about Paulson's comment that he would be surprised if a
> batch compiler could handle Isabelle.  I suppose he could be using `use',
> but that seems strange.

He uses "use" out the wazoo and relies on there being a repl at some points for
user interaction.  Most, if not all, of the uses of "use" can go away by
switching to CM files.  I'm looking into the repl problem to see if some
suitable subset of Isabelle can be built.