| author | haftmann |
| Mon, 08 Dec 2014 12:30:47 +0100 | |
| changeset 59105 | 18d4e100c267 |
| parent 59104 | a14475f044b2 |
| child 59106 | af691e67f71f |
--- 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 ***