--- a/NEWS Wed Jul 20 14:52:09 2016 +0200
+++ b/NEWS Thu Jul 21 10:52:27 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 ***
@@ -103,6 +108,9 @@
* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".
+* Completion templates for commands involving "begin ... end" blocks,
+e.g. 'context', 'notepad'.
+
*** Isar ***
@@ -145,8 +153,8 @@
"method_facts". This is particularly useful for Eisbach method
definitions.
-* Eisbach provides method "use" to modify the main facts of a given
-method expression, e.g.
+* Proof method "use" allows to modify the main facts of a given method
+expression, e.g.
(use facts in simp)
(use facts in \<open>simp add: ...\<close>)