# HG changeset patch
# User wenzelm
# Date 1566040660 -7200
# Node ID 86692888c313aa18a678b43e861c2d88272729cb
# Parent  0c1b08d0b1fe8e5775c35ca4305d99e49ecdd00c
NEWS;

diff -r 0c1b08d0b1fe -r 86692888c313 NEWS
--- a/NEWS	Sat Aug 17 13:16:19 2019 +0200
+++ b/NEWS	Sat Aug 17 13:17:40 2019 +0200
@@ -7,6 +7,23 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Internal derivations record dependencies on oracles and other theorems
+accurately, including the implicit type-class reasoning wrt. proven
+class relations and type arities. In particular, the formal tagging with
+"Pure.skip_proofs" of results stemming from "instance ... sorry" is now
+propagated properly to theorems depending on such type instances.
+
+* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the
+actual proposition that is assumed in the goal and proof context. This
+requires at least Proofterm.proofs = 1 to show up in theorem
+dependencies.
+
+* Command 'thm_oracles' prints all oracles used in given theorems,
+covering the full graph of transitive dependencies.
+
+
 *** Isar ***
 
 * The proof method combinator (subproofs m) applies the method