Am 20.11.2013 um 17:17 schrieb Makarius <[email protected]>: > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
