theory Test imports Main begin;

    theorem my_thm: " A & B --> B & A";

    proof;

        assume " A & B";

        then obtain B and A ..;

        then show  "B & A" ..;

    qed;