Re: [isabelle] Composing BNFs

Hi Lars,

> I checked, but unless I'm missing something, "map_def_of" is just the theorem "x = x".

Of course. The constant stands for an intermediate term.

If you look at the type of "bnf_of_typ", you'll see "unfold_set" as one of the components of the result. This should contain the theorem you are looking for.



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