[isabelle-dev] HOL/Examples vs HOL/ex

[Florian Haftmann]

>   Pure-Examples  --  Notable Examples for Isabelle/Pure.
> 
>   Pure-ex  --  Miscellaneous examples and experiments for Isabelle/Pure.
> 
>   HOL-Examples  --  Notable Examples for Isabelle/HOL.
> 
>   HOL-ex  --  Miscellaneous examples and experiments for Isabelle/HOL.

> We can certainly consolidate this further by promoting a few more
> "miscellaneous examples" to "notable examples": by moving them and
> putting them into proper shape.
> 
> We do need a bin for "miscellaneous examples and experiments", and I
> think the traditional "ex" directories are a good place for that.

My perspective is that »Notable Examples« are supposed to be studied by
a human reader
whereas »miscellaneous examples« check technical abilities of the system.

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220203/19aec655/attachment.sig>