src/HOL/Fun.thy
changeset 4059 59c1422c9da5
parent 2912 3fac3e8d5d3e
child 4648 f04da668581c
     1.1 --- a/src/HOL/Fun.thy	Sat Nov 01 12:58:08 1997 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sat Nov 01 12:59:06 1997 +0100
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  Fun = Set +
     1.6  
     1.7 +instance set :: (term) order
     1.8 +                       (subset_refl,subset_trans,subset_antisym,psubset_eq)
     1.9  consts
    1.10  
    1.11    inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)