# HG changeset patch
# User wenzelm
# Date 1146955627 -7200
# Node ID eb063e7932d7ec3ac770ffc97ac8f2e42d23f88f
# Parent  a14871b57387582dc6b31681b294bebf23b90de2
* Isar: removed obsolete 'concl is' patterns.

diff -r a14871b57387 -r eb063e7932d7 NEWS
--- a/NEWS	Sun May 07 00:44:50 2006 +0200
+++ b/NEWS	Sun May 07 00:47:07 2006 +0200
@@ -129,6 +129,10 @@
 * Isar: 'obtain' takes an optional case name for the local context
 introduction rule (default "that").
 
+* Isar: removed obsolete 'concl is' patterns.  INCOMPATIBILITY, use
+explicit (is "_ ==> ?foo") in the rare cases where this still happens
+to occur.
+
 * Isar/locales: new derived specification elements 'definition',
 'abbreviation', 'axiomatization', which support type-inference, admit
 object-level specifications (equality, equivalence).  See also the