Thanks so much, Vincent! Your tactic/conversion definitely sounds like the
"easy button" I was looking for, and should get me past the cardinality
difficulties I was having. Good thinking with the equality resolution --
I'll be dealing with real numbers soon enough, so I would have encountered
th
n Sun, Nov 4, 2012 at 11:34 AM, Petros Papapanagiotou <
p.papapanagio...@sms.ed.ac.uk> wrote:
> Hello John,
>
>
> On 04/11/2012 03:48, John Nicol wrote:
>
>> Never figured out why
>> real#real is a different type than real*real (they're both just tuples,
>> r
t the
> moment,
> but I'm wondering what {3,4} means in HOL Light. In HOL4 it's a singleton
> list
> holding a pair of numbers.
>
> Konrad.
>
>
>
>
>
>
> On Sat, Nov 3, 2012 at 10:48 PM, John Nicol wrote:
>
>> Hi,
>>
>> I was
Hi,
I was pretty excited and optimistic when I found that HOL Light had
developed a declarative mode, so I started working with the HOL Light
system a few weeks ago. (Without going into the whole philosophy, I prefer
declarative proofs because they're closer to my understanding of proofs,
they're
(whoops, fixing the subject)
John> 1. Error with workaround... "apt-get install" puts Ocaml in a
> John> "nonstandard" location.. /usr/lib/ocaml/camlp5. Specifying this
> John> with "export CAMLP5LIB" fixed the problem. (This was tricky to
> John> find, because there were also libs at /usr/loca
Hi,
I ran into several problems installing HOL Light on Ubuntu 12.04. Googling
around, I found similar problems; any new HOL user with Ubuntu will run
into these, I think. It would be great if the configurations and
documentation could reflect this so other users don't hit this.
I checked out t
