This is the first release of BooleanAlgebrasIntro2, an attempt to formalize
as much of Givant/Halmos' "Introduction to Boolean Algebras" as I can in the
Coq Proof Assistant.  For this release, v0.1, the final theorem was the normal
form theorem for finitely generated subalgebras.  The rest of the package 
was directly translated from earlier portions of the book, and most proofs
follow the same exact logic as the book's, of course with little gaps filled in
wherever they arrive.  Not all of the previous material has been translated into
Coq though, but I'll come back for things like Boolean Rings and interval
algebras in due time.
I recommend reading the philosophical discussion at [index.html] to determine
whether or not you want to risk making your computer too happy by compiling
this.  This compiled fine on Coq 8.4pl4.
To compile, merely unpack the tarball, enter the directory, and type `make`, without the quotes, while making sure that the shell knows the path to the Coq compiler.

Special thanks to Daniel Schepler, who's "Topology" and "Zorn's Lemma" packages
were inlined extensively, and intermittently notated as such.  

Daniel Wyckoff
dwyckoff76@remove.the.obvious.hotmail.notmail.com
