Re: [isabelle] Trying to rename Lattices.thy

On 6/24/2012 2:50 AM, Brian Huffman wrote:
Hi Gottfried,

I tried renaming Lattices.thy to "Attices.thy", as you suggested. It
appears that the errors you get are caused by various locale
predicates (like class.boolean_algebra or class.semilattice_inf)
having different argument orders. If you rearrange the arguments into
the right order again, everything else should work.

I wouldn't want to be rearranging anything in a distribution source to "fix it", but that might be good information for the future.

I have no idea why the the argument order would depend on the theory
name. This seems like a really undesirable "feature".

I would suggest to the other developers...

Thanks for the help. No reason for me to be in the loop beyond this.


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