[isabelle] New AFP entry: Free Boolean Algebra by Brian Huffman


This theory defines a type constructor representing the free Boolean
algebra over a set of generators. Values of type (?)formula represent
propositional formulas with uninterpreted variables from type ?, ordered
by implication. In addition to all the standard Boolean algebra
operations, the library also provides a function for building
homomorphisms to any other Boolean algebra type.

Thanks Brian!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.