# HG changeset patch
# User haftmann
# Date 1418038247 -3600
# Node ID 18d4e100c2676953068f3e6416ec37f4094ff9fb
# Parent  a14475f044b2856ddbe7ebb3e8946ea359644bb4
NEWS

diff -r a14475f044b2 -r 18d4e100c267 NEWS
--- a/NEWS	Fri Dec 05 19:35:36 2014 +0100
+++ b/NEWS	Mon Dec 08 12:30:47 2014 +0100
@@ -22,6 +22,11 @@
 context, without implicit global state.  Potential for accidental
 INCOMPATIBILITY, make sure that required theories are really imported.
 
+* 'find_theorems': search patterns which are abstractions are
+schematcially expanded before search.  Search results match the
+naive expectation more closely, particularly wrt. abbreviations.
+INCOMPATIBILITY.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***