Theory Product_Type; fixed typos
authorhaftmann
Thu Mar 20 12:02:51 2008 +0100 (2008-03-20 ago)
changeset 263559276633fdc24
parent 26354 46c7d00dd4b4
child 26356 2312df2efa12
Theory Product_Type; fixed typos
NEWS
     1.1 --- a/NEWS	Thu Mar 20 12:01:17 2008 +0100
     1.2 +++ b/NEWS	Thu Mar 20 12:02:51 2008 +0100
     1.3 @@ -44,6 +44,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Product_Type: duplicated lemmas split_Pair_apply and injective_fst_snd
     1.8 +removed, use split_eta and prod_eqI instead.  Renamed upd_fst to apfst and upd_snd
     1.9 +to apsnd.  INCOMPATIBILITY.
    1.10 +
    1.11  * Theory Nat: removed redundant lemmas that merely duplicate lemmas of
    1.12  the same name in theory Orderings:
    1.13  
    1.14 @@ -111,7 +115,7 @@
    1.15  definition/function/....  No separate induction rule is provided.  The
    1.16  "primrec" command distinguishes old-style and new-style specifications
    1.17  by syntax.  The former primrec package is now named OldPrimrecPackage.
    1.18 -When adjusting theories, beware: constants stemming for new-style
    1.19 +When adjusting theories, beware: constants stemming from new-style
    1.20  primrec specifications have authentic syntax.
    1.21  
    1.22  * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
    1.23 @@ -1028,7 +1032,7 @@
    1.24      includes Code_Integer.
    1.25    - Code_Index provides an additional datatype index which is mapped to
    1.26      target-language built-in integers.
    1.27 -  - Code_Message provides an additional datatype message_string} which is isomorphic to
    1.28 +  - Code_Message provides an additional datatype message_string which is isomorphic to
    1.29      strings; messages are mapped to target-language strings.
    1.30  
    1.31  * New package for inductive predicates