< User:Boris TsirelsonRevision as of 14:05, 8 August 2010 by imported>Boris Tsirelson
The graphical user interface started.
(CC) Image: Boris Tsirelson The graphical user interface started.
The source file is read.
(CC) Image: Boris Tsirelson The source file is read.
Definitions are processed; the formulation of the first lemma is being processed.
(CC) Image: Boris Tsirelson Definitions are processed; the formulation of the first lemma is being processed.
The formulation of the first lemma is processed; the goal is pending.
(CC) Image: Boris Tsirelson The formulation of the first lemma is processed; the goal is pending.
(CC) Image: Boris Tsirelson At last, a really serious lemma.
(CC) Image: Boris Tsirelson The goal.
(CC) Image: Boris Tsirelson "We have", why?
(CC) Image: Boris Tsirelson Here is why!
(CC) Image: Boris Tsirelson Really complicated arguments...
(CC) Image: Boris Tsirelson Happy end is coming.
(CC) Image: Boris Tsirelson The theorem is proved.
(CC) Image: Boris Tsirelson Some options of the Proof General.
(CC) Image: Boris Tsirelson Isabelle, show us your methods...
(CC) Image: Boris Tsirelson ...and your term bindings...
(CC) Image: Boris Tsirelson ...and the theorems.