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 
instead of the more sensible 
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.