clarified context;

clarified context;

tuned proof;

merged

simps_of_case: Better error if split rule is not an equality

simps_of_case: allow Drule.dummy_thm as ignored split rule

implicit partial divison operation in integral domains

separate class for division operator, with particular syntax added in more specific classes

explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer

dropped dead config option

tuned, including proper signature for functor argument

dropped dead code

explicit argument expansion of uncheck rules; rewriting of user-space type system must behave similarly to abbreviations

explicit input marker for operations

completely separated canonical class abbreviations from abbreviations stemming from non-canonical morphisms -- these have no shared concept

self-contained formulation of abbrev for named targets

correct sort constraints for abbreviations in type classes * * * yet another bunch of corrections

separate function to compute exported abbreviation

clearly separated target primitives (target_foo) from self-contained target operations (foo)

tuned order

dedicated config options to deactivate uncheck phase for improvable syntax

clarified interfaces for improvable syntax

tuned

clarified context;