User:Boris Tsirelson/Sandbox1: Difference between revisions
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| | {{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| | {{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| | {{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| | {{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| | {{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| | {{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| | {{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.}} |