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;

clarified context;

clarified context;

tuned;

discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;

discontinued legacy;

obsolete (see 189c81779a68);

eliminated odd C combinator -- Isabelle/ML usually has canonical argument order;

clarified context;

clarified context;

tuned;

clarified context;

tuned;

obsolete;