NEWS

 
 * Old datatype package:
   * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
     "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
     INCOMPATIBILITY.
-  * The generated constants "xxx_case" and "xxx_rec" have been renamed
-    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
+  * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
+    renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>
+    "case_prod").
     INCOMPATIBILITY.
 
 * The types "'a list" and "'a option", their set and map functions, their
   relators, and their selectors are now produced using the new BNF-based
   datatype package.
   Renamed constants:
     Option.set ~> set_option
     Option.map ~> map_option
     option_rel ~> rel_option
-    list_size ~> size_list
-    option_size ~> size_option
   Renamed theorems:
     set_def ~> set_rec[abs_def]
     map_def ~> map_rec[abs_def]
     Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
     option.recs ~> option.rec

 proofs: Measure functions can be declared by proving a rule of the
 form "is_measure f" and giving it the [measure_function] attribute.
 The "is_measure" predicate is logically meaningless (always true), and
 just guides the heuristic.  To find suitable measure functions, the
 termination prover sets up the goal "is_measure ?f" of the appropriate
-type and generates all solutions by prolog-style backwards proof using
+type and generates all solutions by Prolog-style backward proof using
 the declared rules.
 
 This setup also deals with rules like 
 
   "is_measure f ==> is_measure (list_size f)"