[isabelle-dev] docs for new datatype package

[Jasmin Blanchette]

> 
>> The rule set I’d need is “typ_desc_typ_struct.inducts”, which datatype_compat doesn’t generate.

> The rule you’re looking for is called “compat_a_b_a_list_b_list.induct” (no s).

Actually, it’s the other way around. With the old package, the “inducts” rule is just a collection of four rules, hence the s. These four rules have now separate names. They are assembled together by the “induct … and …” method. Now it’s a bit more tedious, because they have separate names, as you observed. See e.g. this line in “FOL-Fitting” (AFP), which used to use “inducts” (implicitly):

  apply (induct t and ts rule: closedt.induct closedts.induct)

Strangely enough, hardly anybody uses the old “induct” rule, which combines everything together — but that’s the one I referred to in my previous email.

In short, everything should be there, but under different names. “isabelle doc datatype” also documents this.

Jasmin