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

Reply via email to