Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
Generalize the compositional preservation theorems
more specification of the quotient package in IsarRef
specification of the quotient package
Finish localizing the quotient package.
Modernized HOL-Import for HOL Light
HOL/Import more precise map types