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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
