[isabelle-dev] New (Co)datatypes: Status & Plan 2

Makarius makarius at sketis.net
Wed Nov 20 17:17:09 CET 2013

We have a bad state in Isabelle/d983a020489d:

* HOL-BNF_Example fails like this:

*** Theory loader: failed to load "Gram_Lang" (unresolved "DTree")
*** Theory loader: failed to load "Parallel" (unresolved "DTree")
*** Extra variables on rhs: "dtree_unfold"
*** The error(s) above occurred in definition:
*** "unfold rt ct == dtree_unfold rt (the_inv fset o ct)"
*** At command "definition" (line 25 of 

* The "Datatypes" document is broken.

Looking at http://isabelle.in.tum.de/reports/Isabelle/ is odd: spinning 
wheel for 4bc48d713602 (time comment "8 hours ago").

So maybe mira is down or non-terminating.


More information about the isabelle-dev mailing list