equal
deleted
inserted
replaced
36 <p> |
36 <p> |
37 |
37 |
38 <h2><!-- _GP_ distname --></h2> |
38 <h2><!-- _GP_ distname --></h2> |
39 New features in <strong><!-- _GP_ distname --></strong> include |
39 New features in <strong><!-- _GP_ distname --></strong> include |
40 <ul> |
40 <ul> |
|
41 <li>New image HOL4 with imported library from HOL4 system on top of |
|
42 HOL-Complex (about 2500 additional theorems).</li> |
|
43 |
41 <li>New theory Ring_and_Field with over 250 basic numerical laws, |
44 <li>New theory Ring_and_Field with over 250 basic numerical laws, |
42 all proved in axiomatic type classes for semirings, rings and fields.</li> |
45 all proved in axiomatic type classes for semirings, rings and fields.</li> |
43 |
46 |
44 <li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li> |
47 <li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li> |
45 |
48 |