An Example of a Cofinitary Group in Isabelle/HOL

Title:	An Example of a Cofinitary Group in Isabelle/HOL
Author:	Bart Kastermans
Submission date:	2009-08-04
Abstract:	We formalize the usual proof that the group generated by the function k -> k + 1 on the integers gives rise to a cofinitary group.
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.

Older releases: