more class operations for the sake of efficient generated code

merged

back to parallel compression: full AFP build does require 16GB Java heap (reverting 107472ccc60d);

back to pide_session=false for now, requires too many JVM resources (reverting 026de3424c39);

clarified signature;

avoid redundant export handling for build;

prefer single name

more lemmas

build bit operations on word on library theory on bit operations

bit operations as distinctive library theory

tweak for code generation

pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all

more lemmas and less name space pollution

canonical bit shifts for word type, leaving duplicates as they are at the moment

essential instance about bit structure

more transfer rules

dropped yet another duplicate

fundamental construction of word type following existing transfer rules

replaced mere alias by input abbreviation

replaced mere alias by abbreviation

replaced operation with weak abstraction by input abbreviation

avoid compound operation

formal relationships between operations

eliminated warnings

replaced mere alias by input abbreviation

enable pide_session by default;

avoid resource problems of JVM by too many parallel XZ compression tasks;

interpretations for boolean operators

more specific thm reference

clarified errors;