Re: [isabelle] Calling external provers from Isabelle



On Fri, 1 Mar 2013, Lukas Bulwahn wrote:

The implementation is in http://isabelle.in.tum.de/repos/isabelle/file/e6524a89c9e3/src/HOL/Tools/Quickcheck/narrowing_generators.ML Function value and dynamic_value_strict provide the compilation and the execution.

Here is the public release version of that file: http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013/src/HOL/Tools/Quickcheck/narrowing_generators.ML

As a rule of thumb: changset id -> isabelle-dev, proper releases -> isabelle-users.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.