* Isar: removed obsolete 'concl is' patterns.
authorwenzelm
Sun, 07 May 2006 00:47:07 +0200
changeset 19587 eb063e7932d7
parent 19586 a14871b57387
child 19588 846f0d5bfc83
* Isar: removed obsolete 'concl is' patterns.
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