src/HOL/Fun.thy
changeset 5608 a82a038a3e7a
parent 5305 513925de8962
child 5852 4d7320490be4
     1.1 --- a/src/HOL/Fun.thy	Fri Oct 02 10:44:20 1998 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Oct 02 14:28:39 1998 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     1.5  consts
     1.6  
     1.7 -  Id          ::  'a => 'a
     1.8 +  id          ::  'a => 'a
     1.9    o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    1.10    inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    1.11    inj_on      :: ['a => 'b, 'a set] => bool
    1.12 @@ -37,7 +37,7 @@
    1.13  
    1.14  defs
    1.15  
    1.16 -  Id_def	"Id             == %x. x"
    1.17 +  id_def	"id             == %x. x"
    1.18    o_def   	"f o g          == %x. f(g(x))"
    1.19    inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
    1.20    inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"