NEWS
changeset 14224 442c097c1437
parent 14211 7286c187596d
child 14233 f6b6b2c55141
     1.1 --- a/NEWS	Thu Oct 09 18:13:32 2003 +0200
     1.2 +++ b/NEWS	Thu Oct 09 18:20:14 2003 +0200
     1.3 @@ -17,6 +17,12 @@
     1.4    symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
     1.5    existing theory and ML files.
     1.6  
     1.7 +* Pure: Using the functions Theory.add_finals or Theory.add_finals_i
     1.8 +  or the new Isar command "finalconsts", it is now possible to
     1.9 +  make constants "final", thereby ensuring that they are not defined
    1.10 +  later.  Useful for constants whose behaviour is fixed axiomatically
    1.11 +  rather than definitionally, such as the meta-logic connectives.
    1.12 +
    1.13  *** Isar ***
    1.14  
    1.15  * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
    1.16 @@ -42,7 +48,8 @@
    1.17  *** HOL ***
    1.18  
    1.19  * 'specification' command added, allowing for definition by
    1.20 -specification.
    1.21 +  specification.  There is also an 'ax_specification' command that
    1.22 +  introduces the new constants axiomatically.
    1.23  
    1.24  * SET-Protocol: formalization and verification of the SET protocol suite;
    1.25