Re: [isabelle] lattice syntax problems (OR: what does it mean to merge two theories?)
On 07/28/2011 09:26 PM, Brian Huffman wrote:
But in the short term, it would be nice for theory imports to behave
in the way I expect (i.e. actually merge every theory in the import
list, without throwing any away).
One cannot change the semantics of theory merges "in the short term",
just because "no_notation" happens to be conceptually broken. We must
get rid of it, instead of going further in the same direction.
This archive was generated by a fusion of
Pipermail (Mailman edition) and