src/HOL/Fun.thy
changeset 31604 eb2f9d709296
parent 31438 a1c4c1500abe
child 31775 2b04504fcb69
     1.1 --- a/src/HOL/Fun.thy	Wed Jun 10 15:04:32 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Jun 10 15:04:33 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_rep_proofs"}*}
     1.8 +text{*For Proofs in @{text "Tools/datatype_package/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)