theory Exercises1 = Main: lemma "A \ B \ B \ A" oops lemma "\ A \ B; B \ C \ \ A \ C" oops text {* use constdefs to define a new constant @{text or} that defines @{text "\"} by conjunction and negation *} thm notI notE lemma "A \ B \ or A B" apply (unfold or_def) oops thm ccontr lemma "or A B \ A \ B" oops lemma "(\x. \y. P x y) \ (\y. \x. P x y)" oops lemma "((\x. P x) \ Q) \ (\x. P x \ Q)" oops lemma "\x. (P x \ (\x. P x))" oops end