> 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
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
