[isabelle-dev] NEWS: generated code as proper theory export

Lars Hupel hupel at in.tum.de
Fri Feb 1 14:29:45 CET 2019

> In 2012 we eliminated all Makefiles from AFP: I did not know that some
> came back, or chose to ignore it.

~/work/afp (default)$ find thys/ -name Makefile

> The formal status of sessions is defined via "isabelle build" -- that is
> a powerful tool that can do many things. I.e. we can easily define that
> anything outside of it as outside of AFP.

This is the de-facto situation, yes.

More information about the isabelle-dev mailing list