I added some material and ran the HOL distribution locally. This is what I got:
Running HOL-Metis_Examples ... HOL-Metis_Examples FAILED (see also "isabelle build_log -H Error HOL-Metis_Examples") *** Unexpected outcome: "none" *** At command "sledgehammer" (line 19 of "~~/src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.thy") Unfinished session(s): HOL-Metis_Examples If we run this in an interactive session, it fails in the same way. This can’t be connected with the material that I added. Larry _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
