# HG changeset patch
# User skalberg
# Date 1065716414 -7200
# Node ID 442c097c1437cf8f15f73d8bb97e65838f4e3457
# Parent  0ee05eef881bc0d380c674bb8625270ed85dbb8b
Added info on the new 'finalconsts' command.

diff -r 0ee05eef881b -r 442c097c1437 NEWS
--- a/NEWS	Thu Oct 09 18:13:32 2003 +0200
+++ b/NEWS	Thu Oct 09 18:20:14 2003 +0200
@@ -17,6 +17,12 @@
   symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
   existing theory and ML files.
 
+* Pure: Using the functions Theory.add_finals or Theory.add_finals_i
+  or the new Isar command "finalconsts", it is now possible to
+  make constants "final", thereby ensuring that they are not defined
+  later.  Useful for constants whose behaviour is fixed axiomatically
+  rather than definitionally, such as the meta-logic connectives.
+
 *** Isar ***
 
 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
@@ -42,7 +48,8 @@
 *** HOL ***
 
 * 'specification' command added, allowing for definition by
-specification.
+  specification.  There is also an 'ax_specification' command that
+  introduces the new constants axiomatically.
 
 * SET-Protocol: formalization and verification of the SET protocol suite;