Thanks - that looks very useful!
On Fri, Aug 9, 2013 at 8:57 AM, Michael Norrish <
[email protected]> 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 Kumar" <[email protected]> wrote:
>
> 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, HOL4 only has a bit of theory about cardinality of
> finite sets.
> But before I start on porting many of the results above, I'd love to find
> out that I'm wrong...
>
> Anybody know of any theory about cardinality in HOL4, or of its certain
> absence?
>
>
> ------------------------------------------------------------------------------
> Get 100% visibility into Java/.NET code with AppDynamics Lite!
> It's a free troubleshooting tool designed for production.
> Get down to code-level detail for bottlenecks, with <2% overhead.
> Download for free and get started troubleshooting in minutes.
> http://pubads.g.doubleclick.net/gampad/clk?id=48897031&iu=/4140/ostg.clktrk
>
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Get 100% visibility into Java/.NET code with AppDynamics Lite!
It's a free troubleshooting tool designed for production.
Get down to code-level detail for bottlenecks, with <2% overhead.
Download for free and get started troubleshooting in minutes.
http://pubads.g.doubleclick.net/gampad/clk?id=48897031&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
