src/HOL/Fun.thy
changeset 40719 acb830207103
parent 40703 d1fc454d6735
child 40968 a6fcd305f7dc
     1.1 --- a/src/HOL/Fun.thy	Fri Nov 26 20:52:21 2010 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Nov 26 21:09:36 2010 +0100
     1.3 @@ -155,11 +155,6 @@
     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/datatype_rep_proofs"}*}
     1.8 -lemma datatype_injI:
     1.9 -    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
    1.10 -by (simp add: inj_on_def)
    1.11 -
    1.12  theorem range_ex1_eq: "inj f \<Longrightarrow> b : range f = (EX! x. b = f x)"
    1.13    by (unfold inj_on_def, blast)
    1.14