1 2 3 4 5 6 7 8 9 10 11 12
theory Example = Main:; lemma "A --> B --> A"; proof; assume A; show "B --> A"; proof; qed; qed; end;