On Thu, Aug 2, 2012 at 8:03 AM, Bill Richter
rich...@math.northwestern.eduwrote:
Thanks, Ramana and Rob! As Rob says, I don't use new_axiom to define by
type point, but I do use new_axiom to define Hilbert's geometry axioms,
so I took no offense. I would definitely prefer to use neither
Thanks, Ramana! I don't quite understand. In each theorem I should
make an extra hypothesis which will look something like assume
Hilbert_plane H (Between) (===) Line {HP};
And I'll add the label HP to each by list in which I refer to one of
my earlier theorems? In your earlier post, I think
(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
On 03/08/12 07:48, Bill Richter wrote:
Back to my earlier question, my miz3 code begins new_type(point,0);;
new_type_abbrev(point_set,`:point-bool`);;
new_constant(Line,`:point_set-bool`);; I still don't know what the HOL, or
HOL4 meaning of this is, but I have a new conjecture: My new_type
