lemma"((A \ B) \ (A \ C) \ (B \ C)) \ C" apply prop_solver done
method guess_all =
(match premises in U[thin]:"\x. P (x :: 'a)" for P \ \<open>match premises in "?H (y :: 'a)" for y \<Rightarrow> \<open>rule allE[where P = P and x = y, OF U]\<close>
| match conclusion in"?H (y :: 'a)"for y \<Rightarrow> \<open>rule allE[where P = P and x = y, OF U]\<close>\<close>)
lemma"(\x. P(x) \ Q(x)) \ P(z) \ P(y) \ Q(y)" apply (solves \<open>guess_all, prop_solver\<close>) \<comment> \<open>Try it without solve\<close> done
method guess_ex =
(match conclusion in "\x. P (x :: 'a)" for P \ \<open>match premises in "?H (x :: 'a)" for x \<Rightarrow> \<open>rule exI[where x=x]\<close>\<close>)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
