Admin/page/main-content/index.content
changeset 14611 e9d2f771b3c7
parent 14582 f0779f6fa7e8
child 14615 603f08285c65
equal deleted inserted replaced
14610:9c2e31e483b2 14611:e9d2f771b3c7
    42   all proved in axiomatic type classes for semirings, rings and fields.</li>
    42   all proved in axiomatic type classes for semirings, rings and fields.</li>
    43 
    43 
    44 <li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
    44 <li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
    45 
    45 
    46 <li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
    46 <li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
       
    47 
       
    48 <li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>
    47 
    49 
    48 <li>Improved locales (named proof contexts), instantiation of locales.</li>
    50 <li>Improved locales (named proof contexts), instantiation of locales.</li>
    49 
    51 
    50 <li>Improved handling of linear and partial orders in simplifier.</li>
    52 <li>Improved handling of linear and partial orders in simplifier.</li>
    51  
    53