improved mode parser; added mode annotations to examples

moved datatype mode and string functions to the auxillary structure

improving mode parsing in the predicate compiler

improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler

merged

Tidied up some very ugly proofs

small fixes

merged

join entries properly on theory merge

moved some dvd [int] facts to Int

moved algebraic classes to Ring_and_Field

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

standardized filter/filter_out;

modernized some structure names;

eliminated obsolete/unused Thm.kind_internal/is_internal etc.;

modernized functor/structures Interpretation;

tuned whitespace;

unregister: eliminated unused status;

proper header;

proper header; tuned whitespace;

proper header; adapted ResBlacklist -- eliminated inefficient hash table; eliminated some old folds;

separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;

Named_Thms is not scalable;

replaced slightly odd Thm.is_internal by Facts.is_concealed -- as provided by the name space; tuned;

tuned;

tuned proof;

separate "inner_rule" tag indicates parts of induction rules -- avoids unclear overlap with "internal" tag;

removed unused file;