# Re: [isabelle] locales, including documentation & possible programming bugs

Thanks, Brian, that's very helpful!  I was really confused by the
\equiv biz.  Can you explain two more things:

what do the 1000 priorities here even mean: [1000,1000,1000,1000] 70?
If we right a b \cong c d, I want a & b to be bound really tightly
together, so 1000 sounds like a good number, and I want the whole
expression to be bound tighter than say and or implies, so 70 is a
good number.  But then I'd write it as [1000, 70, 1000].

Rules stated in terms of object logic connectives, like "P \<and> Q
--> R", aren't very useful with the "rule" method. You had better
state rules using "==>", like
"P ==> Q ==> R" instead.

I've been puzzled for some time by the preference (especially in
Julien's Tarski geometry Coq code) by folks writing

P ==> Q ==> R ==> S ==> T ==> U
P & Q & R & S & T ==> U .

And you're saying there's a good reason for this!  Great!  Can you
explain why the first approach works better with rules?

--
Best,
Bill



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.