more portable SQL types;

more portable: SQL standard syntax instead of MySQL extension;

general SQL database support, for SQLite and PostgreSQL; tuned;

updated;

minimal support for PostgreSQL databases;

elaborated examples for computations

isabelle update_cartouches

dedicated computation preprocessing rules for nat, int implemented by target language literals

dropped superfluous preprocessing rule

preprocessing rules must always stem from static context

computation preprocessing rules to allow literals as input for computations

dedicated preprocessor for computations

extended syntax allows to include datatype constructors directly in computations

variables and type must be checked before entering evaluation sandwich

more explicit errors in pathological cases

more computation antiquotations

computations and partiality

tuned

more uniform use of Reconstruct.clean_proof_of;

clarified message: print subgoal number instead of potentially large term;

tuned;

suppress warnings uniformly, even in explicit commands 'find_theorems', 'solve_direct';

tuned;

proper background certificate from make_context, which can be a super-theory of the direct join (amending d07464875dd4);

misc tuning;

move mono_neutral_cong from AFP/Deep_Learning/PP_Auxiliary

added veriT preprocessing proof reconstruction example

tuned proof

renaming

added is_empty