equal
deleted
inserted
replaced
935 theorems now have different names, most notably "prime_def" is now |
935 theorems now have different names, most notably "prime_def" is now |
936 "prime_nat_iff". INCOMPATIBILITY. |
936 "prime_nat_iff". INCOMPATIBILITY. |
937 |
937 |
938 * Session Old_Number_Theory has been removed, after porting remaining |
938 * Session Old_Number_Theory has been removed, after porting remaining |
939 theories. |
939 theories. |
|
940 |
|
941 * Session HOL-Types_To_Sets provides an experimental extension of |
|
942 Higher-Order Logic to allow translation of types to sets. |
940 |
943 |
941 |
944 |
942 *** ML *** |
945 *** ML *** |
943 |
946 |
944 * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML |
947 * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML |