[Hol-info] [fm-announcements] Call for Papers: NFM 2014

** The Sixth NASA Formal Methods Symposium http://www.NASAFormalMethods.org/ 29 April - 1 May 2014 NASA Johnson Space Center, Houston, Texas, USA ** Theme of the Symp

Re: [Hol-info] cardinal arithmetic

Thanks - that looks very useful! On Fri, Aug 9, 2013 at 8:57 AM, Michael Norrish < michael.norr...@nicta.com.au> wrote: > There's a chunk of stuff in examples/set-theory/hol_sets/cardinalTheory, > including, for example, the fact that k x k = k. > > Michael > > On 09/08/2013, at 17:15, "Ramana K

Re: [Hol-info] cardinal arithmetic

There's a chunk of stuff in examples/set-theory/hol_sets/cardinalTheory, including, for example, the fact that k x k = k. Michael On 09/08/2013, at 17:15, "Ramana Kumar" wrote: > HOL Light has a decent body of theory about cardinality inequalities and > arithmetic for sets-as-predicates. > F

[Hol-info] cardinal arithmetic

HOL Light has a decent body of theory about cardinality inequalities and arithmetic for sets-as-predicates. For example, see https://code.google.com/p/hol-light/source/browse/trunk/sets.ml#2774 and https://code.google.com/p/hol-light/source/browse/trunk/Library/card.ml#171onwards. As far as I know