On 06/06/2020 11:01, Tobias Nipkow wrote: > > > 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).
Larry, are you going to add HOL-Examples yourself? Otherwise I will do it later today. I have already done it for Pure-Examples (material stemming from HOL-Isar_Examples that was actually for Pure, not HOL): https://isabelle-dev.sketis.net/rISABELLEe5df9c8d9d4b2 Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
