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 new_type nor new_axiom.
I'm using what John set me up with, but I think he thought of
On Thu, Aug 2, 2012 at 8:03 AM, Bill Richter
wrote:
> 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 new_type
> nor new_axiom. I'm
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 /usr/loca
Define a four-argument predicate
Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds /\
...
and use that as a hypothesis on all your theorems.
Thanks, Ramana! The code below indicates that I can get rid of new_axiom
following your suggestion. I should have seen t
On 03/08/12 13:43, Bill Richter wrote:
> I don't know how to get rid of new_type using H and your 4-arg predicate. I
> tried this, and I got the error message # Exception: Failure "term after
> binary operator expected":
> parse_as_infix("===",(12, "right"));; let A1_DEF = new_definition `A1
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
On Fri, Aug 3, 2012 at 4:43 AM, Bill Richter
wrote:
>Define a four-argument predicate
> Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds
> /\
>...
>and use that as a hypothesis on all your theorems.
>
> Thanks, Ramana! The code below indicates that I can get
