(*
    Example proof script for Isabelle Proof General.

    Example2.ML,v 8.0 2004/04/17 23:40:00 da Exp

    Same as Example.ML, except using X-Symbol input tokens.
*)

Goal "A \\<and> B \\<longrightarrow> B \\<and> A";
  by (rtac impI 1);
  by (etac conjE 1);
  by (rtac conjI 1);
  by (assume_tac 1);
  by (assume_tac 1);
qed "and_comms";