Re: [isabelle] Trying to rename Lattices.thy
On 6/24/2012 2:50 AM, Brian Huffman wrote:
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