equal
deleted
inserted
replaced
904 
904 
905 * Session HOLLibrary: theory Complete_Partial_Order2 provides reasoning 
905 * Session HOLLibrary: theory Complete_Partial_Order2 provides reasoning 
906 support for monotonicity and continuity in chaincomplete partial orders 
906 support for monotonicity and continuity in chaincomplete partial orders 
907 and about admissibility conditions for fixpoint inductions. 
907 and about admissibility conditions for fixpoint inductions. 
908 
908 
909 * Session HOLLibrary: theory Polynomial contains also derivation of 
909 * Session HOLLibrary: 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 HOLLibrary: theory Sublist provides function "prefixes" with 
916 * Session HOLLibrary: theory Sublist provides function "prefixes" with 
916 the following renaming 
917 the following renaming 
917 
918 
918 prefixeq > prefix 
919 prefixeq > prefix 