an extensive example for lift_bnf across quotients

extension of lift_bnf to support quotient types

unfold intermediate (internal) pred definitions

corrected some confusing terminology / notation

Ramsey with multiple colours and arbitrary exponents

a few new and tidier proofs (mostly about finite sets)

clarified signature: store full theory name;

merged

moved lemmas

merged

suppress record types: not working properly;

removed junk;

discontinued somewhat pointless options;

tuned signature;

clarified signature;

export datatypes;

clarified modules;

misc tuning and clarification: proper check of datatype kind;

clarified modules;

cleaning

tuned

separated Affine theory from Convex

merged

tuned

proper table data structure

removed some vain declarations

merged

made Starlike independent of Abstract_Limits

more direct accessors for simpset

regular merge with no historization, in accordance with regular update

moved starlike where it belongs

merged

clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many small messages stacking up, e.g. when loading HOL-Analysis.Analysis.thy into Isabelle/jEdit;

moved segment lemmas where they belong

merged

moved lemmas

merged

two new theorems

moved lemma

made internal name generation in case expressions more robust

merged

clarified export of consts: recursion is accessible via spec_rules;

more operations;

Removed orphaned theory from HOL-Analysis

merged

clarified position for spec rule: like entity;

clarified name: avoid clashes;

proper dynamic position of application context, e.g. relevant for 'global_interpretation';

proper treatment of variable names;

proper spec_rule name via naming/binding/Morphism.binding;

more informative spec rules;

more robust;

more informative export;

tuned signature -- following Export_Theory.Spec_Rule in Scala;

tuned comment;

clarified export of spec rules: more like locale;

formal position for spec rule (not significant for equality);

proper spec rules via resulting def_thm, e.g. relevant for "isabelle build -o export_theory";

proper spec rules via fun_lhs, e.g. relevant for "isabelle build -o export_theory";

tuned -- avoid confusion of fun_t with fun_lhs;

avoid shadowing of local bindings -- more maintainable;

export spec rules;

Reorganised HOL-Complex_Analysis

split off metric spaces part of Function_Topology: subsequent theories Product_Topology, T1_Spaces, Lindelof_Spaces are purely topological

merged

tuned Analysis manual

tuned Analysis manual

more rules

tuned material

tuned manual

Removed duplicate theorems from HOL-Analysis

Flattened dependency tree of HOL-Analysis

Merged

Simplified Harmonic_Numbers

Split off new HOL-Complex_Analysis session from HOL-Analysis

merged

tuned Analysis/Analysis;

characterization of typical bit operations

merged

renamed Analysis/Winding_Numbers to Winding_Numbers_2; reorganised Analysis/Cauchy_Integral_Theorem by splitting it into Contour_Integration, Winding_Numbers,Cauchy_Integral_Theorem and Cauchy_Integral_Formula.

transfer rule for bit operation

characterization of singleton bit operation

bit accessor and fundamental properties

merged

more informative spec rules: optional name; clarified signature; more thorough treatment of Thm.trim_context vs. Thm.transfer;

proper theory context, e.g. for Thm.transfer;

more structural integrity;

tuned

reduced imports; deleted unusewd minor lemmas for that purpose

tuned

reduced imports and removed unused material

tuned

merged

reduced imports

Fixed a few messy proofs and adjusted inconsistent section headings

A more informative comment

Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.

Remove diagnostic command 'print_dependencies'.

support for output messages;

tuned;

tuned -- avoid deprecated constructors;

tuned signature;

avoid vacuous session Pure -- dump does not read_pure_theory;

updated to polyml-5.8.1-20191113 test version (Poly/ML 055f20cdc326);

clarified vacuous selection vs. Pure;

tuned signature;

tuned theory structure

more robust: size varies due to different position information in "isabelle build" vs. "isabelle dump";

clarified signature;

tuned proofs;

clarified error: tmp file can be invalid in odd situations;

more robust: file length can be invalid in odd situations;

tuned;

tuned whitespace

proper prefix syntax

removed unused auxiliary lemmas

tuned;

added document antiquotation @{system_option};

improved performance of session exports via bulk transactions;

tuned signature;