\<chi> is now considered a letter;
authorwenzelm
Tue Dec 04 21:09:37 2007 +0100 (2007-12-04)
changeset 2552226851f8bdf14
parent 25521 6cebd2ff3ab7
child 25523 08b0feb07239
\<chi> is now considered a letter;
tuned;
NEWS
     1.1 --- a/NEWS	Tue Dec 04 13:22:55 2007 +0100
     1.2 +++ b/NEWS	Tue Dec 04 21:09:37 2007 +0100
     1.3 @@ -4,25 +4,33 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Symbol \<chi> is now considered a letter.  Potential INCOMPATIBILITY
    1.10 +in identifier syntax etc.
    1.11 +
    1.12 +
    1.13  *** Pure ***
    1.14  
    1.15 -* Command "instance" now takes list of definitions in the same
    1.16 -manner as the "definition" command.  Most notably, object equality is now
    1.17 +* Command "instance" now takes list of definitions in the same manner
    1.18 +as the "definition" command.  Most notably, object equality is now
    1.19  possible.  Type inference is more canonical than it used to be.
    1.20  INCOMPATIBILITY: in some cases explicit type annotations are required.
    1.21  
    1.22  
    1.23  *** HOL ***
    1.24  
    1.25 -* Library/Multiset: {#a, b, c#} is new short syntax for {#a#} + {#b#} + {#c#}.
    1.26 -
    1.27 -* Constants "card", "internal_split",  "option_map" now with authentic syntax.
    1.28 -
    1.29 -* Definitions subset_def, psubset_def, set_diff_def, Compl_def, le_bool_def,
    1.30 -less_bool_def, le_fun_def, less_fun_def, inf_bool_def, sup_bool_def,
    1.31 -Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, Inf_fun_def, Sup_fun_def,
    1.32 -inf_set_def, sup_set_def, Inf_set_def, Sup_set_def, le_def, less_def,
    1.33 -option_map_def now with object equality.
    1.34 +* Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
    1.35 +
    1.36 +* Constants "card", "internal_split", "option_map" now with authentic
    1.37 +syntax.
    1.38 +
    1.39 +* Definitions subset_def, psubset_def, set_diff_def, Compl_def,
    1.40 +le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def,
    1.41 +sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def,
    1.42 +Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def,
    1.43 +Sup_set_def, le_def, less_def, option_map_def now with object
    1.44 +equality.
    1.45  
    1.46  
    1.47