src/HOL/Ord.thy
changeset 5889 d3ecef6b5682
parent 4640 ac6cf9f18653
child 5953 d6017ce6b93e
equal deleted inserted replaced
5888:d8e51792ca85 5889:d3ecef6b5682
     5 
     5 
     6 Type classes for order signatures and orders.
     6 Type classes for order signatures and orders.
     7 *)
     7 *)
     8 
     8 
     9 Ord = HOL +
     9 Ord = HOL +
       
    10 
       
    11 (*FIXME move to HOL.thy*)
       
    12 setup Classical.setup
       
    13 setup attrib_setup
    10 
    14 
    11 axclass
    15 axclass
    12   ord < term
    16   ord < term
    13 
    17 
    14 global
    18 global