src/HOL/Hilbert_Choice.thy
changeset 33014 85d7a096e63f
parent 32988 d1d4d7a08a66
child 33057 764547b68538
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Oct 20 11:36:19 2009 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 20 13:20:42 2009 +0200
     1.3 @@ -91,6 +91,9 @@
     1.4  
     1.5  subsection {*Function Inverse*}
     1.6  
     1.7 +lemma inv_def: "inv f = (%y. SOME x. f x = y)"
     1.8 +by(simp add: inv_onto_def)
     1.9 +
    1.10  lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
    1.11  apply (simp add: inv_onto_def)
    1.12  apply (fast intro: someI2)