NEWS
changeset 55183 17ec4a29ef71
parent 55152 a56099a6447a
child 55289 30d874dc7000
     1.1 --- a/NEWS	Thu Jan 30 14:28:04 2014 +0100
     1.2 +++ b/NEWS	Thu Jan 30 14:37:53 2014 +0100
     1.3 @@ -114,6 +114,14 @@
     1.4  * Theory reorganizations:
     1.5    * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
     1.6  
     1.7 +* Sledgehammer:
     1.8 +  - Renamed options:
     1.9 +      isar_compress ~> compress_isar
    1.10 +      isar_try0 ~> try0_isar
    1.11 +    INCOMPATIBILITY.
    1.12 +
    1.13 +* Try0: Added 'algebra' and 'meson' to the set of proof methods.
    1.14 +
    1.15  * The symbol "\<newline>" may be used within char or string literals
    1.16  to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
    1.17