User:Boris Tsirelson/Sandbox1: Difference between revisions

Revision as of 15:50, 8 August 2010

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

The graphical user interface started.

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

The source file is read.

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

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.

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.

@@ Line 1: / Line 1: @@
-[http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle]
+[http://www.cse.unsw.edu.au/~kleing/top100/#1 Top 100 theorems in Isabelle] +
-[http://www.cs.ru.nl/~freek/100/ Formalizing 100 Theorems]
+[http://www.cs.ru.nl/~freek/100/ Formalizing 100 Theorems] +
+[http://isabelle.in.tum.de/ Isabelle] +
+[http://isabelle.in.tum.de/download.html Download and installation] +
+[http://isabelle.in.tum.de/projects.html Projects] +
+[http://isabelle.in.tum.de/library/ The Isabelle2009-2 Library] +
+[http://isarmathlib.org/ IsarMathLib: A library of formalized mathematics for Isabelle/ZF]
 {{Image|Isabelle1.png|right|350px|The graphical user interface started.}}