[isabelle-dev] NEWS: Proof methods "simp" and "simp_all" in Pure

[Makarius]

*** General ***

* Pure provides basic versions of proof methods "simp" and "simp_all"
that only know about meta-equality (==). Potential INCOMPATIBILITY in
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
is relevant to avoid confusion of Pure.simp vs. HOL.simp.


This refers to Isabelle/b01154b74314. It means that "unfold" /
'unfolding' does not have to be abused for general simplification in
examples based on Pure.


	Makarius