[isabelle-dev] New (Co)datatypes: Status & Plan 2
jasmin.blanchette at gmail.com
Wed Nov 20 18:32:38 CET 2013
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.
More information about the isabelle-dev