[isabelle-dev] HOL-ex

[Makarius]

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 <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).

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