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: | ||
[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.}} | {{Image|Isabelle1.png|right|350px|The graphical user interface started.}} |
Revision as of 15:50, 8 August 2010
Top 100 theorems in Isabelle + Formalizing 100 Theorems + Isabelle + Download and installation + Projects + The Isabelle2009-2 Library + IsarMathLib: A library of formalized mathematics for Isabelle/ZF
The graphical user interface started.
The source file is read.
Definitions are processed; the formulation of the first lemma is being processed.
The formulation of the first lemma is processed; the goal is pending.