While doing an 'isabelle makeall all' on my local machine, I
encountered the error
Sledgehammering...
*** Unexpected outcome: "unknown".
*** At command "sledgehammer" (line 26 of
"/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy")
I guess I lack some sort of heavy equipment here. What surprises me
is that on macbroy2 I don't have set up sledgehammer either, but I
don't get this error.
Clemens
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
