Theory monoid-comm

theory file

name monoid-comm
version 1.16
requires
meta.description Commutative monoids
meta.author Joe Leslie-Hurd <joe@gilith.com>
meta.license MIT
meta.provenance HOL Light theory extracted on 2015-10-13
meta.show "Algebra.Monoid"
meta.show "Data.Bool"
meta.show "Data.List"
meta.show "Number.Natural"
meta.hol-light-int-file hol-light.int
name main
imports
  • thm
  • mult
subs
5 subs
name monoid-witness
package monoid-witness-1.9
name monoid-thm
imports
  • monoid-witness
package monoid-thm-1.6
name monoid-mult
imports
  • monoid-witness
  • monoid-thm
package monoid-mult-1.13
name thm
imports
  • monoid-witness
package monoid-comm-thm-1.8
name mult
imports
  • monoid-mult
package monoid-comm-mult-1.5
[evaluating…]