Changes to complete distributive lattices due to Viorel Preoteasa

lots of new material, ultimately related to measure theory

more symbols;

ran isabelle update_op on all sources

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

simple new lemmas, mostly about sets

discontinued theory-local special syntax for lattice orderings

--HG--
extra : rebase_source : a43595e983fb7b5e8e9031a09ddee560d27e761b

tuned proof;

misc tuning and modernization;

lots of new theorems about differentiable_on, retracts, ANRs, etc.

more theorems

tuned proofs;

Moved material from AFP/Randomised_Social_Choice to distribution

explicit property for unbreakable block;

more canonical names

prefer abbreviations for compound operators INFIMUM and SUPREMUM

retain ASCII syntax for output, when HOL/Library/Lattice_Syntax is not present (amending e96292f32c3c);

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";

prefer symbols for "Union", "Inter";

isabelle update_cartouches -c -t;

add various lemmas

isabelle update_cartouches;

tuned whitespace;

Convex hulls: theorems about interior, etc. And a few simple lemmas.

rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity

--HG--
extra : rebase_source : 6c7faec3b6fc45b9da856e08add46f99a0b483b7

modernized header uniformly as section;

more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

--HG--
extra : rebase_source : 8664c1d86ed72607199cc8197a480070514ae330

Sup/Inf on functions decoupled from complete_lattice.

more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)

--HG--
extra : rebase_source : 710314bbc990dc6cb912a800546a75f7c3a07dca

subsumed by existing default simp rules for functions and booleans

--HG--
extra : rebase_source : ef9788dcfe4feeb0d38628d1d5a9fe004fb0b659

generalized and strengthened cong rules on compound operators, similar to 1ed737a98198

elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION

consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly

normalising simp rules for compound operators

dropped redundant theorems

monotonicity in complete lattices

bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
* * *
tuned

add equalities for SUP and INF over constant functions

add SUP and INF for conditionally complete lattices

generalize SUP and INF to the syntactic type classes Sup and Inf

killed most "no_atp", to make Sledgehammer more complete

tuned proofs -- clarified flow of facts wrt. calculation;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

factored syntactic type classes for bot and top (by Alessandro Coglio)

weaker precendence of syntax for big intersection and union on sets

explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts

fundamental revision of big operators on sets

generalized subclass relation;
tuned proof

complete_linorder is also a complete_distrib_lattice

move auxiliary lemmas from Library/Extended_Reals to HOL image

simp results for simplification results of Inf/Sup expressions on bool;
tuned proofs

tuned proofs

tuned simpset

retain syntax here

--HG--
extra : rebase_source : e0404cbbb00948257c361a89d62100a9adf74571

tuned syntax declarations; tuned structure

--HG--
extra : rebase_source : 1b6c21e91abe00bbf0ca93b6c0f5a24da0bef488

marked candidates for rule declarations

moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax

reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems

distributed lattice properties of predicates to places of instantiation

--HG--
extra : rebase_source : f060e45b06e82cc14c73eba231a21e4636bbe179

use Inf/Sup_bool_def/apply as code equations

--HG--
extra : rebase_source : 9822efe22960d359544f837617d3e6e106e3d18a

fundamental theorems on Set.bind

--HG--
extra : rebase_source : f60f78a12efe9f4496619a04d48afb38f7eccb9d

lattice type class instances for `set`; added code lemma for Set.bind

official status for UN_singleton

removed legacy lemmas in Complete_Lattices

removed further legacy rules from Complete_Lattices

tuned proofs

remove some redundant [simp] declarations;
simplify some proofs;

tune proofs

tune simpset for Complete_Lattices

renamed Complete_Lattices lemmas, removed legacy names

renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.

--HG--
rename : src/HOL/Complete_Lattice.thy => src/HOL/Complete_Lattices.thy