Drop rewrite rule arguments of sublocale and interpretation implementations.

Proper rewrite morphisms in locale instances.

command 'interpret' no longer exposes resulting theorems as literal facts;

Experimental support for rewrite morphisms in locale instances.

provide explicit variant initializers for regular named target vs. almost-named target

tuned signature;

clarified positions, e.g. for reports on literal facts;

tuned whitespace;

tuned;

tuned;

tuned signature;

unfold is subject to unfold_abs_def (still inactive);
tuned signature;

eliminated unused argument (see also 58110c1e02bc);

abandoned attempt to unify sublocale and interpretation into global theories

clarified terminology

--HG--
extra : rebase_source : 7d6250e9779271e6fab8427461c710c747e36885

alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism

prefer conventional read/check distinction over manual check

clarified role of context for reading rewrite specifications

formally correct context for export, which got screwed up in 87203a0f0041

tuned whitespace

explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory

--HG--
extra : rebase_source : e70bdb7735cabc4cfe7dbef6845f65ac7756c8b2

make SML/NJ happy;

clarified contexts by factoring out reading and definition of mixins

formally correct context for export

tuned whitespace

represent both algebraic and local-theory views on locale interpretation in interfaces

--HG--
extra : rebase_source : 0f233aa5dd88ebb1594d03af4f3a3d7b08a44fa7

tuned -- share implementations as far as appropriate

--HG--
extra : rebase_source : 3ba2e010f554aa31e06b635a8086472f922f8805

coalesce permanent_interpretation.ML with interpretation.ML

--HG--
extra : rebase_source : 580d89700ffeaf7aa823f4bcc4e638cca8ce081d

separate ML module for interpretation

--HG--
extra : rebase_source : 867de135491ddc9e949d932384cce64f60343123