Proofs.thy

(* using tactics *)
lemma "A ∧ B ⟶ B ∧ A"
  apply (rule impI)  (* A ∧ B ⟹ B ∧ A *)
  apply (rule conjI) (* 1: A ∧ B ⟹ B and 2: A ∧ B ⟹ A *)
(* goal 1 *)
   apply (erule conjE) (* A ⟹ B ⟹ B *)
   apply assumption
(* goal 2 *)
   apply (erule conjE) (* A ⟹ B ⟹ A *)
  apply assumption
  done

(* using Isar *)
lemma "A ∧ B ⟶ B ∧ A"
proof (rule impI)
  assume 1: "A ∧ B"
  show "B ∧ A"
  proof
    from 1 show "A"
      by (rule conjE)
    from 1 show "B"
      by (rule conjE)
  qed
qed