src/HOL/Fun.thy
changeset 12338 de0f4a63baa5
parent 12258 5da24e7e9aba
child 12459 6978ab7cac64
     1.1 --- a/src/HOL/Fun.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  Fun = Typedef +
     1.6  
     1.7 -instance set :: (term) order
     1.8 +instance set :: (type) order
     1.9                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
    1.10  consts
    1.11    fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"