NEWS
changeset 23129 a318773dca05
parent 23116 16e1401afe91
child 23180 80b9caed2ba8
equal deleted inserted replaced
23128:8e0abe0fa80f 23129:a318773dca05
   540     HOL.abs ~> HOL.minus_class.abs
   540     HOL.abs ~> HOL.minus_class.abs
   541     HOL.divide ~> HOL.divide_class.divide
   541     HOL.divide ~> HOL.divide_class.divide
   542     Nat.power ~> Nat.power_class.power
   542     Nat.power ~> Nat.power_class.power
   543     Nat.size ~> Nat.size_class.size
   543     Nat.size ~> Nat.size_class.size
   544     Numeral.number_of ~> Numeral.number_class.number_of
   544     Numeral.number_of ~> Numeral.number_class.number_of
       
   545     FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf
       
   546 
       
   547 * Rudimentary class target mechanims involves constant renames:
       
   548 
       
   549     Orderings.min ~> Orderings.ord_class.min
       
   550     Orderings.max ~> Orderings.ord_class.max
       
   551     FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
   545 
   552 
   546 * case expressions and primrec: missing cases now mapped to "undefined"
   553 * case expressions and primrec: missing cases now mapped to "undefined"
   547 instead of "arbitrary"
   554 instead of "arbitrary"
   548 
   555 
   549 * new constant "undefined" with axiom "undefined x = undefined"
   556 * new constant "undefined" with axiom "undefined x = undefined"
   576     class "comp_lat" now named "complete_lattice"
   583     class "comp_lat" now named "complete_lattice"
   577 
   584 
   578     Instantiation of lattice classes allows explicit definitions
   585     Instantiation of lattice classes allows explicit definitions
   579     for "inf" and "sup" operations.
   586     for "inf" and "sup" operations.
   580 
   587 
   581   INCOMPATIBILITY. Theorem renames:
   588   INCOMPATIBILITY.  Theorem renames:
   582 
   589 
   583     meet_left_le            ~> inf_le1
   590     meet_left_le            ~> inf_le1
   584     meet_right_le           ~> inf_le2
   591     meet_right_le           ~> inf_le2
   585     join_left_le            ~> sup_ge1
   592     join_left_le            ~> sup_ge1
   586     join_right_le           ~> sup_ge2
   593     join_right_le           ~> sup_ge2