src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Fun.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -117,7 +117,7 @@
 
 definition
   bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
-  [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
+  [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
 
 constdefs
   surj :: "('a => 'b) => bool"                   (*surjective*)