User:Boris Tsirelson/Sandbox1: Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Boris Tsirelson
No edit summary
imported>Boris Tsirelson
No edit summary
Line 1: Line 1:
{{Image|Isabelle1.png|right|350px|The graphical user interface started.}}
{{Image|Isabelle1.png|right|350px|The graphical user interface started.}}


{{Image|Isabelle2.png|right|350px|The source file is read.}}
{{Image|Isabelle2.png|left|350px|The source file is read.}}


{{Image|Isabelle3.png|right|350px|Definitions are processed; the formulation of the first lemma is being processed.}}
{{Image|Isabelle3.png|right|350px|Definitions are processed; the formulation of the first lemma is being processed.}}


{{Image|Isabelle4.png|right|350px|The formulation of the first lemma is processed; the goal is pending.}}
{{Image|Isabelle4.png|left|350px|The formulation of the first lemma is processed; the goal is pending.}}


{{Image|Isabelle5.png|right|350px|At last, a really serious lemma.}}
{{Image|Isabelle5.png|right|350px|At last, a really serious lemma.}}


{{Image|Isabelle6.png|right|350px|The goal.}}
{{Image|Isabelle6.png|left|350px|The goal.}}


{{Image|Isabelle7.png|right|350px|"We have", why?}}
{{Image|Isabelle7.png|right|350px|"We have", why?}}


{{Image|Isabelle8.png|right|350px|Here is why!}}
{{Image|Isabelle8.png|left|350px|Here is why!}}


{{Image|Isabelle9.png|right|350px|Really complicated arguments...}}
{{Image|Isabelle9.png|right|350px|Really complicated arguments...}}


{{Image|Isabelle10.png|right|350px|Happy end is coming.}}
{{Image|Isabelle10.png|left|350px|Happy end is coming.}}


{{Image|Isabelle11.png|right|350px|The theorem is proved.}}
{{Image|Isabelle11.png|right|350px|The theorem is proved.}}


{{Image|Isabelle12.png|right|350px|Some options of the Proof General.}}
{{Image|Isabelle12.png|left|350px|Some options of the Proof General.}}


{{Image|Isabelle13.png|right|350px|Isabelle, show us your methods...}}
{{Image|Isabelle13.png|right|350px|Isabelle, show us your methods...}}


{{Image|Isabelle14.png|right|350px|...and your term bindings...}}
{{Image|Isabelle14.png|left|350px|...and your term bindings...}}


{{Image|Isabelle15.png|right|350px|...and the theorems.}}
{{Image|Isabelle15.png|right|350px|...and the theorems.}}

Revision as of 13:56, 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
...and your term bindings...
(CC) Image: Boris Tsirelson
...and the theorems.
Retrieved from "https://citizendium.org/wiki/index.php?title=User:Boris_Tsirelson/Sandbox1&oldid=628819"