[isabelle-dev] HOL-ex

Makarius makarius at sketis.net
Mon Jun 8 22:12:50 CEST 2020

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.


More information about the isabelle-dev mailing list