Am 18.10.2011 um 08:54 schrieb Lukas Bulwahn: > Florian and I are not sure if code_inline or code_unfold fit better to the > intended behaviour of "rewriting a code equation by some simplifying > equation" (unfolding a term by its definition, or inlining the definition).
I would also vote for "code_unfold", if nothing else for consistency with the similar "nitpick_unfold" tag. When I introduced "nitpick_unfold" I also considered "nitpick_inline", but concluded that the "unfold" terminology is from theorem proving and the "inline" terminology from the world of compilers. For the code generator, the argument swings both ways, though... Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
