*** 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev