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.

Alex





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