> Does it really fully unregister? Not fully: (I believe) it unregisters only the non-nested occurrences, e.g. “a” and “b” in my previous example (several emails ago). For “a list” and “b list”, there is some hope, since the old package used to do it right (keeping them apart from the fully polymorphic “list” type).
> Declaring my manual rules as > > lemmas typ_desc_typ_struct_inducts [case_names ..., induct type] = > typ_desc_induct typ_struct_induct typ_list_induct typ_dt_pair_induct > > overwrote the standard list induction rule (because typ_list_induct has > conclusion “P (x :: ‘a some_thing list)”. However, declaring > > declare list.induct [induct type] > > afterwards, brings back the list induction rule and seems to keep > typ_list_induct around - at least it seems to be different to never having > declared typ_list_induct as induct rule at all. > > I’m pretty much poking in the dark here, though. I briefly looked at the code > of the induct method and then remembered why I never wanted to do that again.. Hm, that’s interesting. :S But irrespective of that, there’s a clash for “a” and “b” between the old rule and the new rule. I see no much point in registering the old-style compatibility “a list” and “b list” (or “‘a something list”) induction theorems if we have the new style ones for “a” and “b”. For the AFP, I bit the bullet and wrote “rule:” every single time. With a lemma collection, this shouldn’t be too painful (I did the whole AFP and Isabelle *without* lemma collections even) and will ease the transition away from the compatibility stuff later (e.g. by grepping for “compat_”). Being explicit in cases like this seems like a good idea considering that this is probably not the last time you (guys) will be touching that formalization. It’s also easier because these attributes are wacky, as you noticed yourself. ;) Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
