1 theory Test imports Main begin;
2 theorem my_thm: " A & B --> B & A";
3 proof;
4 assume " A & B";
5 then obtain B and A ..;
6 then show "B & A" ..;
7 qed;