On 05/06/2020 13:43, Lawrence Paulson wrote:
On 5 Jun 2020, at 12:29, Makarius <[email protected]> wrote: HOL-ex has always been an odd bin for very mixed material. I don't see a reason to delete that: otherwise we would have to question other odd sessions, too. We could rather leave HOL-ex as is, and move some of the better examples into a new session HOL-Examples (with material from other sessions, like HOL-Isar_Examples).You make a good point. The start of all this is that I am looking for a home for my Ackermann development (attached). It actually demonstrates the use of the function package with a partial function definition and later proving that it is defined everywhere.
Why don't you start off HOL-EXamples with precisely this theory? Once a start has been made, suitable material can be moved from HOL-ex. As Makarius wrote, some of it is a mixture between real examples and regression tests. I would be liberal and move theories that have some exemplary aspect as well as regression tests (eg Functions).
Tobias
Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
