[isabelle-dev] HOL-ex

[Lawrence Paulson]

> On 5 Jun 2020, at 12:29, Makarius <makarius at sketis.net> 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