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

[Jasmin Blanchette]

Am 20.11.2013 um 17:17 schrieb Makarius <makarius at sketis.net>:

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

Fixed, sorry. I've become way too reliant on mira, which is often down these days, and too aggressive in my pushes.

Jasmin