dropped now obsolete hint;
a few words on theory IArray;
dropped reference to obsolete theory Efficient_Nat

attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary

systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char

coercions between base types can be lifted to sets

annotate obtains with types

merge

made check for conjecture skolemization sound

use safe var index

merged

more type class instances for Numeral_Type (contributed by Jesus Aransay)