[isabelle-dev] HOL-ex

[Tobias Nipkow]

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,
>> 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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5579 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200606/49c8db4c/attachment.bin>