[isabelle-dev] HOL-ex

[Makarius]

On 08/06/2020 15:51, Lawrence Paulson wrote:

>> On 8 Jun 2020, at 14:20, Makarius <makarius at sketis.net> wrote:
>>
>> 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):

There is now a HOL-Examples session in
https://isabelle-dev.sketis.net/rISABELLEebcae4a19e78 --- for now I have moved
the most notable of my usual examples, including the material in the
Documentation/Examples panel of Isabelle/jEdit.


> I had been waiting to check whether others agreed with Tobias’s proposal.
>
> I see that I forgot the attachment, so here it is.

Ackermann.thy looks like a fine entry for HOL-Examples, and I leave it to you
to add it yourself.


	Makarius