--- a/NEWS Wed Jul 20 21:26:11 2016 +0200
+++ b/NEWS Wed Jul 20 22:36:10 2016 +0200
@@ -52,6 +52,11 @@
* Proof method "blast" is more robust wrt. corner cases of Pure
statements without object-logic judgment.
+* 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.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***