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 l /\ ~Collinear (A,B,C) [H1];
thus A,B same_side l \/ B,C same_side l \/ A,C same_side l
proof
(A,B same_side l \/ B,C same_side l) \/ A,C same_side l
proof
assume ~(A,B same_side l \/ B,C same_side l);
~(A,B same_side l) /\ ~(B,C same_side l) [H2] by -;
[...]
I don't think I should need the first line of the proof, which just
inserts a pair of parenthesis. I think this should have worked:
let TwosidesTriangle2aLine_THM = thm `;
let A B C be point;
let l be point_set;
assume Line l /\ ~Collinear (A,B,C) [H1];
thus A,B same_side l \/ B,C same_side l \/ A,C same_side l
proof
assume ~(A,B same_side l \/ B,C same_side l);
~(A,B same_side l) /\ ~(B,C same_side l) [H2] by -;
[...]
It's not that big a deal: 3 extra lines to the proof and almost 100
lines of code indented an extra 2 space. But I would have thought
that miz3 (which seems very smart to me) would understand that
alpha \/ beta \/ gamma
is equivalent to
~alpha /\ ~beta ==> gamma
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
