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