equal
deleted
inserted
replaced
5 |
5 |
6 This release provides many improvements and a few substantial advances over |
6 This release provides many improvements and a few substantial advances over |
7 Isabelle2003. The most prominent highlights of Isabelle2004 are as follows |
7 Isabelle2003. The most prominent highlights of Isabelle2004 are as follows |
8 (see the NEWS of the distribution for more details): |
8 (see the NEWS of the distribution for more details): |
9 |
9 |
|
10 |
|
11 * New image HOL4 with imported library from HOL4 system on top of |
|
12 HOL-Complex (about 2500 additional theorems). |
10 |
13 |
11 * New theory Ring_and_Field with over 250 basic numerical laws, |
14 * New theory Ring_and_Field with over 250 basic numerical laws, |
12 all proved in axiomatic type classes for semirings, rings and fields. |
15 all proved in axiomatic type classes for semirings, rings and fields. |
13 |
16 |
14 * Type "rat" of the rational numbers available in HOL-Complex. |
17 * Type "rat" of the rational numbers available in HOL-Complex. |