adding simplification patterns to multiset simprocs

renaming multiset simprocs

implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion

explicit operations for executable primality checks

more fun without recdef

merged

proper transaction for PostgreSQL;

clarified Date storage;

more operations;

tuned signature;

clarified signature;

renamings

tuning

timestamp string format for SQLite;

support for type Date;

tuned;

tuned;

support for type Boolean;

clarified signature; tuned toString;

remote database access via ssh port forwarding;

clarified handling of SQL.Type;

clarified toString;

clarified modules;

only intercept regular exceptions

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

misc tuning and modernization;

tuned

merged

tuned

Merged

Simplified Gamma_Function

proper priority queue spec

misc tuning and modernization;

added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;

tuned proofs;

tuned proof;

tuned whitespace;

Added new / improved tactics for fields and rings

Corrected type of dummy pattern

split balance into two, clearer etc

ML antiquotation for generated computations

tuned

tuned structure and terminology

tuned scope of lazy computation

tuned data structure

dropped dead code

tuned name

removed unclear clause; slower but clearer

removed contribution by Daniel Stuewe, too detailed.

added concise log height bound lemma

updated package;

tuned;

tuned

dropped dead code

ensure no duplicates after preprocessing

reject polymorphic result types; formally generalized to multiple result types

explicit a-priori detection of unsuitable terms for computations

more options;

tuned;

experimental computations: use arbitrary generated code for RHSs, not just constants

tuned documentation

merged

updated to jdk-8u121;

clarified owner;

insist in proper GNU tar, to avoid subtle semantic differences;

hardlink within JVM; clarified file attributes;

tuned;

clarified operation: include dirs as well;

tuned;

tuned;

build_jdk in Scala;

corrected static scope: multi-argument composition does not apply partially

less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic

tuned;

added postorder

tuned

int version slicker

tuned

tuned

clarified theory name; tuned;

New material from Bertrand's postulate (file Bertrand_Discrete_Sqrt), and tidied an old messy proof

tuned

removed some old ASCII syntax;

prefer context groups;

misc tuning and modernization;

prefer context groups;

more symbols;

misc tuning and modernization;

isabelle update_cartouches -c -t;

more symbols via abbrevs;

tuned signature;