equal
deleted
inserted
replaced
946 theorems now have different names, most notably "prime_def" is now |
946 theorems now have different names, most notably "prime_def" is now |
947 "prime_nat_iff". INCOMPATIBILITY. |
947 "prime_nat_iff". INCOMPATIBILITY. |
948 |
948 |
949 * Session Old_Number_Theory has been removed, after porting remaining |
949 * Session Old_Number_Theory has been removed, after porting remaining |
950 theories. |
950 theories. |
|
951 |
|
952 * Session HOL-Types_To_Sets provides an experimental extension of |
|
953 Higher-Order Logic to allow translation of types to sets. |
951 |
954 |
952 |
955 |
953 *** ML *** |
956 *** ML *** |
954 |
957 |
955 * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML |
958 * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML |