src/HOL/Fun.thy
changeset 28562 4e74209f113e
parent 27330 1af2598b5f7d
child 28711 60e51a045755
     1.1 --- a/src/HOL/Fun.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -117,7 +117,7 @@
     1.4  
     1.5  definition
     1.6    bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
     1.7 -  [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
     1.8 +  [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
     1.9  
    1.10  constdefs
    1.11    surj :: "('a => 'b) => bool"                   (*surjective*)