equal
deleted
inserted
replaced
14 This supersedes functor Named_Thms, but with a subtle change of |
14 This supersedes functor Named_Thms, but with a subtle change of |
15 semantics due to external visual order vs. internal reverse order. |
15 semantics due to external visual order vs. internal reverse order. |
16 |
16 |
17 |
17 |
18 *** HOL *** |
18 *** HOL *** |
|
19 |
|
20 * Command and antiquotation "value" provide different evaluation slots (again), |
|
21 where the previous strategy (nbe after ML) serves as default. |
|
22 Minor INCOMPATIBILITY. |
19 |
23 |
20 * New (co)datatype package: |
24 * New (co)datatype package: |
21 - Renamed theorems: |
25 - Renamed theorems: |
22 disc_corec ~> corec_disc |
26 disc_corec ~> corec_disc |
23 disc_corec_iff ~> corec_disc_iff |
27 disc_corec_iff ~> corec_disc_iff |