I had a look and it should work now in 1cdd27b5d78a (with Isabelle2016-RC0). I do not know what exactly went wrong or what caused the failure. The problem seems to be related to some change in theory imports. It seems as if code_pred cannot retrieve the specification of a constant under certain import orders, but I am not familiar enough with these Isabelle internals to pinpoint the problem.

Andreas

On 30/12/15 00:20, Makarius wrote:
AFP/CoreC++ is broken (already quite some time).

The current situation:

Isabelle/a70b89a3e02e
AFP/a2c981ab8d39

CoreC++ FAILED
*** Failed to load theory "CoreC++" (unresolved "Execute")
*** No such predicate: "SubObj.path_via"
*** At command "code_pred" (line 214 of 
"~/isabelle/afp-devel/thys/CoreC++/Execute.thy")


     Makarius

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to