John, I apologize for a bad bug report yesterday, and also exceeding
the 40KB message limit. I can handle axiom B3 fine, and I now have my
Hilbert axiomatic geometry miz3 code on my web page at
http://www.math.northwestern.edu/~richter/OpenIntervalHilbertAxiom.ml
I think I found a miz3 bug.
I'm using HOL4 in the Windows console. I load a file using the use
command, like this:
use E:/E_main2/binp/HOL4k7/examples/euclid.sml;
I then edit some ML scripts in an editor and load them into HOL4 using
the use command. My scripts get errors, so when I try to load
euclid.sml again as shown
Colin, let me see if I understand. You hacked the Makefile so that you
use (as I did) pa_j_3.1x_6.02.2.ml And then `make' succeeds, but you
get a warning `pattern-matching is not exhaustive'?
Thank you Bill. Yes, 'make' completes, giving at least the following error
messages/warnings:
CICM 2012 - Conference on Intelligent Computer Mathematics
July 9-13, 2012 at Jacobs University, Bremen, Germany
http://www.informatik.uni-bremen.de/cicm2012/
Call for participation
As computers and
hey. kindly send us a link from where we download moscow ML on linux.
because we do not get proper installation steps.
--
Best regards,
Aisha Khan,
BEE5-A,
SEECS-NUST.
--
Live Security Virtual Conference
Exclusive live
Hello everyone!
A couple of weeks ago, I asked a couple of questions on this list regarding
an exercise on formal power series that I had been working on. I now got
around to writing up what I have learned in a blog post:
http://blog.felixbreuer.net/2012/06/11/hol.html
Thanks again to
On Mon, Jun 11, 2012 at 1:12 AM, gottfried.bar...@gmx.com wrote:
I'm using HOL4 in the Windows console. I load a file using the use
command, like this:
use E:/E_main2/binp/HOL4k7/examples/euclid.sml;
On windows I usually run HOL4 under emacs. But of course that's
just personal preference.
On 6/11/2012 12:26 PM, Konrad Slind wrote:
On Mon, Jun 11, 2012 at 1:12 AM,gottfried.bar...@gmx.com wrote:
On windows I usually run HOL4 under emacs. But of course that's
just personal preference.
I tried to load hol-mode.el in xemacs running under Cygwin, but I
couldn't get it to work.
Send (or post) a minimal failing version and the maintainers can help
you.
I thought it was me causing problems by loading my own scripts after
HOL/examples/euclid.sml, but it wasn't.
The failure comes from making the divides constant an infix after its
definition. All is fine the first time
Please follow the instructions at
http://hol.sourceforge.net/InstallKananaskis.html
(This includes a download link for Moscow ML.)
By the way, on Linux I'd strongly recommend using Poly/ML instead; it's much
faster.
If things go wrong, please post copies of the errors you get, and we can
On Mon, Jun 11, 2012 at 10:45 PM, Michael Norrish
michael.norr...@nicta.com.au wrote:
Please follow the instructions at
http://hol.sourceforge.net/InstallKananaskis.html
(This includes a download link for Moscow ML.)
By the way, on Linux I'd strongly recommend using Poly/ML instead; it's
On 12/06/12 08:03, Ramana Kumar wrote:
On Mon, Jun 11, 2012 at 10:45 PM, Michael Norrish
michael.norr...@nicta.com.au
mailto:michael.norr...@nicta.com.au wrote:
Please follow the instructions at
http://hol.sourceforge.net/InstallKananaskis.html
(This includes a download link
I've made Konrad's suggested change in the repository so that users of future
releases won't hit the same problem.
You can see the revised file at
https://raw.github.com/mn200/HOL/e8110e6d9c03e54685f30f216357f77ef380b8f2/examples/euclid.sml
Best,
Michael
On 12/06/12 05:29, Konrad Slind wrote:
On 6/11/2012 7:36 PM, Michael Norrish wrote:
I'm glad you got the emacs mode to work. There’s some (recently
updated) documentation for it at
http://hol.sourceforge.net/hol-mode.html
I used (load holdir/tools/hol-mode) from that file, and the 3
Emacs commands at this FAQ page link to
John Freek, I found a real bug (the code below), an inference error
that miz3 should report but does not. I think miz3 calculates some
result ~(A = B), but the `by' mechanism malfunctions, as ~(A = B) is
used even though it's not given by a `by' justification.
BTW I've formalized my Hilbert
Thus, it may be reasonable to conclude that I have now successfully
built HOL Light.
Excellent, Colin! Yeah, if you're not getting strange bugs, you
should conclude this.
What are you using HOL Light in order to do?
I'd like to code up an early auction theory result due to
John Freek, here's a minor bug (really a new feature I desire) in
the last thm of my 1200 lines of Hilbert geometry axiom code
http://www.math.northwestern.edu/~richter/OpenIntervalHilbertAxiom.ml
let TwosidesTriangle2aLine_THM = thm `;
let A B C be point;
let l be point_set;
assume Line
John Freek, I'm sorry, I just goofed, I really want to get rid of
two lines of code, not just one. Here's the last thm of
http://www.math.northwestern.edu/~richter/OpenIntervalHilbertAxiom.ml
let TwosidesTriangle2aLine_THM = thm `;
let A B C be point;
let l be point_set;
assume Line l /\
18 matches
Mail list logo
