changeset 63118 | 80c361e9d19d |
parent 63116 | 32492105b015 |
parent 63117 | acb6d72fc42e |
child 63121 | 284e1802bc5c |
--- a/NEWS Mon May 23 18:04:45 2016 +0200 +++ b/NEWS Mon May 23 22:43:22 2016 +0200 @@ -199,6 +199,8 @@ pave way for a possible future different type class instantiation for polynomials over factorial rings. INCOMPATIBILITY. +* Library/Sublist.thy: renamed prefixeq -> prefix and prefix -> strict_prefix + * Dropped various legacy fact bindings, whose replacements are often of a more general type also: lcm_left_commute_nat ~> lcm.left_commute