> 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. Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
