Re: [isabelle] Composing BNFs



Hi Lars,

> For my particular use case, that's not a problem. But I can't find the
> definition of that constant, which means I can't unfold it. Is the
> definition recorded somewhere?

Look for "xxx_def_of_bnf" in "bnf_def.ML", for suitable values of "xxx". But you should ask yourself whether you really need to unfold it or if you shouldn't instead rely on the abstract properties given by the BNF (the xxx_of_bnf functions returning "thm").

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.