Flyspeck I: Tame Graphs

 

Title:	Flyspeck I: Tame Graphs
Author:	Gertrud Bauer and Tobias Nipkow
Submission date:	2006-05-22
Abstract:	These theories present the verified enumeration of tame plane graphs as defined by Thomas C. Hales in his proof of the Kepler Conjecture. For explanations see the IJCAR 2006 paper by Nipkow, Bauer and Schultz.
Status: [ok]	This is the development version of this entry generated for Isabelle-25-Dec-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-Flyspeck-Tame-2009-04-29.tar.gz Isabelle 2008: afp-Flyspeck-Tame-2008-06-10.tar.gz Isabelle 2007: afp-Flyspeck-Tame-2008-01-04.tar.gz