Re: [isabelle] Calling external provers from Isabelle



Hi Moa,

> 1) Call Isabelle's code generator to produce a Haskell file of a given
theory.

as a first entry try

	Code_Target.produce_code …

This should suffice for a proof of concept.

Building code from own snippets and generated code is a black art on its
own -- if your project evolves into something persistent, get back here
and I'll try my best to provide you with the most robust and convenient
ways available to arrange things then.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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