theory my_theory imports Main begin thm impI lemma trivial: "A \ A" apply (rule impI) apply assumption done (* of lemma *) thm trivial lemma t2: "A \ B \ B \ C \ A \ C" thm impI apply (rule impI) (* \A \ B; B \ C; A\ \ C*) thm impE apply (rule impE) apply assumption apply assumption (* \A \ B; B \ C; A; B\ \ C *) thm impE apply (rule_tac P="B" and Q = "C" in impE) (* prefer 3*) apply assumption apply assumption apply assumption done end (* of theory file *)