--- a/src/HOL/Fun.thy Sat Nov 01 12:58:08 1997 +0100
+++ b/src/HOL/Fun.thy Sat Nov 01 12:59:06 1997 +0100
@@ -8,6 +8,8 @@
Fun = Set +
+instance set :: (term) order
+ (subset_refl,subset_trans,subset_antisym,psubset_eq)
consts
inj, surj :: ('a => 'b) => bool (*inj/surjective*)