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

[Makarius]

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 
"~~/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy")

* 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.


 	Makarius