On 11/14/2011 09:35 PM, Florian Haftmann wrote:
@Florian: Is it imaginable to add such unsound setup
in a way that it does not infect the evaluation oracle by default?
Indeed. More on that another time (when I find some time).
Florian
@Johannes: If you aim at adding another code target for this theory, I
can assist with the setup.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev