src/HOL/Ord.thy
changeset 2624 ab311b6e5e29
parent 2608 450c9b682a92
child 3143 d60e49b86c6a
equal deleted inserted replaced
2623:6a7372c9ca0f 2624:ab311b6e5e29
     1 (*  Title:      HOL/Ord.thy
     1 (*  Title:      HOL/Ord.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Type class for order signatures.
     6 Type classes for order signatures and orders.
     7 *)
     7 *)
     8 
     8 
     9 Ord = HOL +
     9 Ord = HOL +
    10 
    10 
    11 axclass
    11 axclass