tuned document;

eliminated old fold;

renamed InfixName to Infix etc.;

discontinued unnamed infix syntax;

eliminated unnamed infixes;

apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target

clarifed type

optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program

formal markup of constants;

modernized structures;