nipkow at in.tum.de
Sat Jun 6 11:01:12 CEST 2020
On 05/06/2020 13:43, Lawrence Paulson wrote:
>> 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,
>> 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
> 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).
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev