clarified signature;
more careful treatment of implicit context;

tuned messages;

misc tuning and clarification, notably wrt. flow of context;

isabelle update -u control_cartouches;

proper naming conventions for contexts;

permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;

tuned spelling;

tuned whitespace and sections;

tuned -- eliminated clone;

ran isabelle update_op on all sources

reorder some steps in the construction to support mutual datatypes

@{command_spec} is superseded by @{command_keyword};

tuned signature -- prefer qualified names;

renamed "pairself" to "apply2", in accordance to @{apply 2};

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

modernized setup;

updated to named_theorems;

store explicitly quotient types with no_code => more precise registration of code equations

more appropriate name (Lifting.invariant -> eq_onp)

left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)

more antiquotations;

rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user

implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules

make SML/NJ happy

correct merging of restore data

restoring Transfer/Lifting context

make ML function for deleting quotients public

make SML/NJ happy

use only one data slot; rename print_quotmaps to print_quot_maps; tuned

stronger reflexivity prover

proper use of "member", without embarking on delicate questions about SML equality types;

made SML/NJ happy;

lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided

generate a parameterized correspondence relation

prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

quot_del attribute, it allows us to deregister quotient types

infrastructure that makes possible to prove that a relation is reflexive

added a basic sanity check for quot_map

use a quot_map theorem attribute instead of the complicated map attribute

hide the invariant constant for relators: invariant_commute infrastracture

new package Lifting - initial commit