User:Boris Tsirelson/Sandbox1: Difference between revisions

Revision as of 13:53, 8 August 2010

(CC) Image: Boris Tsirelson
The graphical user interface started.

(CC) Image: Boris Tsirelson
The source file is read.

(CC) Image: Boris Tsirelson
Definitions are processed; the formulation of the first lemma is being processed.

(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
Add image caption here.

@@ Line 21: / Line 21: @@
 {{Image|Isabelle11.png|right|350px|The theorem is proved.}}
-{{Image|Isabelle12.png|right|350px|Add image caption here.}}
+{{Image|Isabelle12.png|right|350px|Some options of the Proof General.}}
-{{Image|Isabelle13.png|right|350px|Add image caption here.}}
+{{Image|Isabelle13.png|right|350px|Isabelle, show us your methods...}}
 {{Image|Isabelle14.png|right|350px|Add image caption here.}}
 {{Image|Isabelle15.png|right|350px|Add image caption here.}}