> >> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
