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

[Brian Huffman]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> a) Keeping theory imports minimal vs. reducing the number of merges
>
> Careful thinking what the logical preliminaries of a particular theory
> are is a necessary, valuable and fruitful task -- I would by no means
> encourage to develop the HOL theories as a structureless coagulation.
>
> That, in order to reduce the number of merges, there are some
> recommended "wasp-waists" in the HOL theory dependencies, does only
> superficially conflict with this: add the appropriate import (Plain,
> Main) to the theory if necessary, and the job is done.  When a
> rearranging of theories is to be done, the proper minimal imports are
> reconstructible quite easily -- in the worst case using an interactive
> session.

I'm afraid I don't understand why reducing the number of merges by  
adding "wasp-waists" is beneficial. From what I understand, adding  
additional theory dependencies could only reduce opportunities for  
parallel execution. Is there another technical reason why the amount  
of merging needs to be limited?

- Brian