src/HOL/Set.ML
changeset 3909 e48e2fb8b895
parent 3905 4bbfbb7a2cd3
child 3912 4ed64ad7fb42
equal deleted inserted replaced
3908:4f19a40a9343 3909:e48e2fb8b895
   599 
   599 
   600 (*Frequently b does not have the syntactic form of f(x).*)
   600 (*Frequently b does not have the syntactic form of f(x).*)
   601 val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
   601 val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
   602 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
   602 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
   603 qed "image_eqI";
   603 qed "image_eqI";
   604 (* Addsimps [image_eqI];
   604 Addsimps [image_eqI];
   605    breaks Auth: together with shrK_neq in Shared.ML it loops.  :-(
       
   606 *)
       
   607 
   605 
   608 bind_thm ("imageI", refl RS image_eqI);
   606 bind_thm ("imageI", refl RS image_eqI);
   609 
   607 
   610 (*The eta-expansion gives variable-name preservation.*)
   608 (*The eta-expansion gives variable-name preservation.*)
   611 val major::prems = goalw thy [image_def]
   609 val major::prems = goalw thy [image_def]