On 08/06/2020 15:51, Lawrence Paulson wrote: >> On 8 Jun 2020, at 14:20, Makarius <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
