equal
deleted
inserted
replaced
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] |