| changeset 59105 | 18d4e100c267 |
| parent 59058 | a78612c67ec0 |
| child 59112 | e670969f34df |
--- 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 ***