[isabelle-dev] A better policy for the typerep class

[Brian Huffman]

Quoting Makarius <makarius at sketis.net>:

> In particular, merging
> ATP_Linkup is a bit critical: if it is done via several unrelated paths,
> then some internal derivations are duplicated unnecessarily.  (In fact, it
> used to crash here in the past, now it only wastes resources.)

I remember a comment that used to be in ATP_Linkup.thy, saying that it  
was required to be either a descendant or ancestor of every other  
theory. I guess this is no longer a requirement, but it seems like you  
are saying it is still strongly recommended.

If this is so, then maybe it is a good idea to move ATP_Linkup so that  
it is imported by Plain? I know that some library theories import only  
Plain and Presburger, for example; if ATP_Linkup were included with  
Plain, it might avoid wasting resources in those cases.

- Brian