blob: c213de4db97a2839b12870bcae382a79d954bdab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
theory Example = Main:;
lemma and_comms: "A & B --> B & A";
proof;
assume "A & B";
show "B & A";
proof;
from prems; show B; ..;
from prems; show A; ..;
qed;
qed;
end;
|