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

[Tobias Nipkow]

>> 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.
> 
> I've discussed that with Florian to some degree.  He made a good job in 
> reorganizing the HOL theory graph, without having to include ATP_Linkup in 
> Plain.

Although a small core is generally a good idea, I frequently have the
problem of proving something with metis in some theory derived from
Main, but not being able to move those proofs into most Main theories,
because metis is not available there. Having metis earlier would be much
appreciated.

I know that metis and ATP_Linkup are different cattles of fish, and I
feel less often the need to call s/h while in some Main theory, although
the ability would no hurt.

Tobias