equal
deleted
inserted
replaced
904 |
904 |
905 * Session HOL-Library: theory Complete_Partial_Order2 provides reasoning |
905 * Session HOL-Library: theory Complete_Partial_Order2 provides reasoning |
906 support for monotonicity and continuity in chain-complete partial orders |
906 support for monotonicity and continuity in chain-complete partial orders |
907 and about admissibility conditions for fixpoint inductions. |
907 and about admissibility conditions for fixpoint inductions. |
908 |
908 |
909 * Session HOL-Library: theory Polynomial contains also derivation of |
909 * Session HOL-Library: theory Library/Polynomial contains also |
910 polynomials but not gcd/lcm on polynomials over fields. This has been |
910 derivation of polynomials (formerly in Library/Poly_Deriv) but not |
911 moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave |
911 gcd/lcm on polynomials over fields. This has been moved to a separate |
912 way for a possible future different type class instantiation for |
912 theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible |
913 polynomials over factorial rings. INCOMPATIBILITY. |
913 future different type class instantiation for polynomials over factorial |
|
914 rings. INCOMPATIBILITY. |
914 |
915 |
915 * Session HOL-Library: theory Sublist provides function "prefixes" with |
916 * Session HOL-Library: theory Sublist provides function "prefixes" with |
916 the following renaming |
917 the following renaming |
917 |
918 |
918 prefixeq -> prefix |
919 prefixeq -> prefix |