[isabelle-dev] Spec_Check

[Makarius]

On Thu, 30 May 2013, Makarius wrote:

>  * Canonical session name?  It looks like the name of the tool is
>    "Spec_Check", according to its main Spec_Check.thy
>
>    So it would be session HOL-Spec_Check in ~~/src/HOL/Spec_Check/
>
>    You still have a chance to rename "Spec_Check" now, before anything is
>    pushed to main Isabelle.  The directory location is given by having a
>    session built on HOL, though.

Now that everything is in-place (and SML/NJ partially happy in 
2bbeab01c0ea) I have realized that despite the import of theory HOL/Main, 
the tool does not depend on HOL at all.

So it could just import Pure, and then be session Spec_Check in 
~~/src/Tools/Spec_Check/.

Thus it would conform to the idea of a general Quickcheck tool for 
Isabelle/ML -- understanding "Isabelle/ML" as the brand name for this 
cutting-edge Standard ML implementation.

Of course we should avoid repeated alternation of source locations. So 
there is a second chance here, but then it should be really right.


 	Makarius