# HG changeset patch
# User wenzelm
# Date 1204748647 -3600
# Node ID d3363a8547083075bd7526b240298fd513631435
# Parent  6bae051e8b7e23405a8f27cf55775a3943a52fd7
indexing literal facts: exclude background context;

diff -r 6bae051e8b7e -r d3363a854708 NEWS
--- a/NEWS	Wed Mar 05 21:24:06 2008 +0100
+++ b/NEWS	Wed Mar 05 21:24:07 2008 +0100
@@ -31,6 +31,12 @@
 See HOL/Complex/Complex.thy for an Isar example and
 HOL/Library/Eval.thy for an ML example.
 
+* Indexing of literal facts: be more serious about including only
+facts from the visible specification/proof context, but not the
+background context (locale etc.).  Affects `prop` notation and method
+"fact".  INCOMPATIBILITY: need to name facts explicitly in rare
+situations.
+
 
 *** HOL ***