NEWS
changeset 62335 e85c42f4f30a
parent 62332 eeaa2f7b5329
child 62343 24106dc44def
child 62354 fdd6989cc8a0
     1.1 --- a/NEWS	Wed Feb 17 15:41:28 2016 +0100
     1.2 +++ b/NEWS	Wed Feb 17 17:08:36 2016 +0100
     1.3 @@ -27,6 +27,10 @@
     1.4      "bnf" outputs a new proof obligation expressing pred in terms of set
     1.5         (not giving a specification for pred makes this one reflexive)
     1.6      INCOMPATIBILITY: manual "bnf" declarations may need adjustment
     1.7 +  - Renamed lemmas:
     1.8 +      rel_prod_apply ~> rel_prod_inject
     1.9 +      pred_prod_apply ~> pred_prod_inject
    1.10 +    INCOMPATIBILITY.
    1.11  
    1.12  
    1.13  New in Isabelle2016 (February 2016)