changeset 31604 | eb2f9d709296 |
parent 31438 | a1c4c1500abe |
child 31775 | 2b04504fcb69 |
--- a/src/HOL/Fun.thy Wed Jun 10 15:04:32 2009 +0200 +++ b/src/HOL/Fun.thy Wed Jun 10 15:04:33 2009 +0200 @@ -133,7 +133,7 @@ shows "inj f" using assms unfolding inj_on_def by auto -text{*For Proofs in @{text "Tools/datatype_rep_proofs"}*} +text{*For Proofs in @{text "Tools/datatype_package/datatype_rep_proofs"}*} lemma datatype_injI: "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)" by (simp add: inj_on_def)