equal
deleted
inserted
replaced
369 |
369 |
370 txt\<open> |
370 txt\<open> |
371 @{subgoals[display,indent=0,margin=65]} |
371 @{subgoals[display,indent=0,margin=65]} |
372 |
372 |
373 applying @text{someI} automatically instantiates |
373 applying @text{someI} automatically instantiates |
374 @{term f} to @{term "\<lambda>x. SOME y. P x y"} |
374 \<^term>\<open>f\<close> to \<^term>\<open>\<lambda>x. SOME y. P x y\<close> |
375 \<close> |
375 \<close> |
376 |
376 |
377 by (rule someI) |
377 by (rule someI) |
378 |
378 |
379 (*both can be done by blast, which however hasn't been introduced yet*) |
379 (*both can be done by blast, which however hasn't been introduced yet*) |