equal
deleted
inserted
replaced
393 * HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and |
393 * HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and |
394 ~~/src/HOL/Algebra/poly. Existing theories should be based on |
394 ~~/src/HOL/Algebra/poly. Existing theories should be based on |
395 ~~/src/HOL/Library/Polynomial instead. The latter provides |
395 ~~/src/HOL/Library/Polynomial instead. The latter provides |
396 integration with HOL's type classes for rings. INCOMPATIBILITY. |
396 integration with HOL's type classes for rings. INCOMPATIBILITY. |
397 |
397 |
398 * HOL/BNF: |
398 * HOL-BNF: |
399 - Various improvements to BNF-based (co)datatype package, including |
399 - Various improvements to BNF-based (co)datatype package, including |
400 new commands "primrec_new", "primcorec", and |
400 new commands "primrec_new", "primcorec", and |
401 "datatype_new_compat", as well as documentation. See |
401 "datatype_new_compat", as well as documentation. See |
402 "datatypes.pdf" for details. |
402 "datatypes.pdf" for details. |
403 - New "coinduction" method to avoid some boilerplate (compared to |
403 - New "coinduction" method to avoid some boilerplate (compared to |