NEWS
changeset 40128 ac0935cfcbc4
parent 40118 be8acf6e63bb
parent 40127 e4f1275820b2
child 40162 7f58a9a843c2
--- a/NEWS	Mon Oct 25 13:36:20 2010 +0200
+++ b/NEWS	Mon Oct 25 16:18:00 2010 +0200
@@ -6,6 +6,8 @@
 
 *** General ***
 
+* Significantly improved Isabelle/Isar implementation manual.
+
 * Explicit treatment of UTF8 sequences as Isabelle symbols, such that
 a Unicode character is treated as a single symbol, not a sequence of
 non-ASCII bytes as before.  Since Isabelle/ML string literals may
@@ -317,6 +319,10 @@
 
 *** ML ***
 
+* Antiquotation @{assert} inlines a function bool -> unit that raises
+Fail if the argument is false.  Due to inlining the source position of
+failed assertions is included in the error output.
+
 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
 meaning.