new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions

some new material, also recasting some theorems using “obtains”

Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion

backed out unintended effects of 8355a6e2df79 in src/HOL/Algebra

more complete program generation in presence of dictionaries

removed obsolete test -- coincides with mainline version;

updated to polyml-5.7 pre-release from repository;

use the cancellation simprocs directly

don't activate simproc on cancel_comm_monoid_add

cancellation simprocs generalising the multiset simprocs

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