src/HOL/Fun.thy
changeset 31775 2b04504fcb69
parent 31604 eb2f9d709296
child 31949 3f933687fae9
--- a/src/HOL/Fun.thy	Tue Jun 23 12:09:14 2009 +0200
+++ b/src/HOL/Fun.thy	Tue Jun 23 12:09:30 2009 +0200
@@ -133,7 +133,7 @@
   shows "inj f"
   using assms unfolding inj_on_def by auto
 
-text{*For Proofs in @{text "Tools/datatype_package/datatype_rep_proofs"}*}
+text{*For Proofs in @{text "Tools/Datatype/datatype_rep_proofs"}*}
 lemma datatype_injI:
     "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
 by (simp add: inj_on_def)