Hi Leo, Am 04.07.2014 um 07:48 schrieb Leo Freitas <leo.frei...@newcastle.ac.uk>:
> I was playing with HOL-Word to see if I could bring some discharged VCs from > another tool into Isabelle. > When I tried sledgehammer on it I got the error message for Z3 Thanks for the report! We will look into this. It may take some time because of a deadline, though. And do let us know should you run into more issues with Z3 (which we upgraded to 4.3 from 3.2 in this version, requiring a major overhaul of our infrastructure). Cheers, Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
