| changeset 3896 | ee8ebb74ec00 |
| parent 3842 | b55686a7b22c |
| child 3905 | 4bbfbb7a2cd3 |
--- a/src/HOL/Set.ML Thu Oct 16 14:00:20 1997 +0200 +++ b/src/HOL/Set.ML Thu Oct 16 14:12:15 1997 +0200 @@ -601,6 +601,7 @@ val prems = goalw thy [image_def] "[| b=f(x); x:A |] ==> b : f``A"; by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1)); qed "image_eqI"; +(* FIXME: Addsimps [image_eqI];*) bind_thm ("imageI", refl RS image_eqI);