equal
deleted
inserted
replaced
337 assumes "p:EX! x. P(x)" |
337 assumes "p:EX! x. P(x)" |
338 and "!!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R" |
338 and "!!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R" |
339 shows "?a : R" |
339 shows "?a : R" |
340 apply (insert assms(1) [unfolded ex1_def]) |
340 apply (insert assms(1) [unfolded ex1_def]) |
341 apply (erule exE conjE | assumption | rule assms(1))+ |
341 apply (erule exE conjE | assumption | rule assms(1))+ |
|
342 apply (erule assms(2), assumption) |
342 done |
343 done |
343 |
344 |
344 |
345 |
345 (*** <-> congruence rules for simplification ***) |
346 (*** <-> congruence rules for simplification ***) |
346 |
347 |