Hi Thomas, Am 13.01.2014 um 13:38 schrieb Thomas Sewell <[email protected]>:
> The change requires, for instance, about a dozen lines of changes to the > files in HOL/Library, which contain about 50K lines of proof, or 3 lines of > changes to HOL/Bali, with 30K. The change to the Nominal examples (30K), > however, is a bit longer (100 changes) and a bit more unpleasant. I've also > checked the change against one chunk of L4.verified, with 70K lines in it, > and have around 60 lines of changes to make. From my perspective, this level > of impact seems to be annoying but not too annoying. I'm interested in what > others think. Your suggested change looks very reasonable to me. However, if possible, it would be nice if the old behavior could be kept via a flag -- unless it's easy to simulate reliably (e.g. using "thin_rl"). One reason for my concern is that the new (co)datatype package's tactics rely extensively on "hyp_subst_tac" and we currently don't have enough tests in the repository to catch all failures. Cheers, Jasmin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
