[isabelle-dev] NEWS: unfold_abs_def

[Makarius]

*** General ***

* The command 'unfolding' and proof method "unfold" include a second
stage where given equations are passed through the attribute "abs_def"
before rewriting. This ensures that definitions are fully expanded,
regardless of the actual parameters that are provided. Rare
INCOMPATIBILITY in some corner cases: use proof method (simp only:)
instead, or declare [[unfold_abs_def = false]] in the proof context.


This refers to Isabelle/52235c27538c. Typical updates can be seen in
AFP/48cee34f4dfa, but this is just the tail-end of similar updates from
some months ago.

The idea to upgrade "unfold" like that is already quite old, but now it
is implemented in a minimally invasive fashion: omitting the old phase 1
and doing phase 2 only breaks many proofs due to odd shifts of bound
variables, beta/eta redexes etc.


Note that the new 'define' command requires the changed behavior of
"unfold" occasionally, because it prefers arguments applied instead of
abstracted in the specification, just like 'definition'.


	Makarius