strengthened type class for bit operations

tuned whitespace;

prefer named lemmas -- more compact proofterms;

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

ran isabelle update_op on all sources

discontinued theory-local special syntax for lattice orderings

--HG--
extra : rebase_source : a43595e983fb7b5e8e9031a09ddee560d27e761b

formal passive interpretation proofs for conj and disj

--HG--
extra : rebase_source : 2435eb0e495ed87fe580548ef966997d83f05541

misc tuning and modernization;

misc tuning and modernization;

boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes

--HG--
extra : rebase_source : 4542f54b0b7fe6c0bea5be2116706e4cfacadaf0

isabelle update_cartouches -c -t;

cancel complementary terms as arguments to sup/inf in boolean algebras

qualifier is mandatory by default;

tuned proofs -- less legacy;

eliminated \<Colon>;

isabelle update_cartouches;

explicit equivalence for strict order on lattices

modernized header uniformly as section;

explicit distributivity facts on min/max

postponed min/max lemmas until abstract lattice is available

prefer abstract simp rule

more lemmas on abstract lattices

tuning and augmentation of min/max lemmas;
more lemmas and simp rules for abstract lattices with order;
tuned proofs

rationalize imports

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

examples for interpretation into target

added lemma

more uniform style for interpretation and sublocale declarations

--HG--
extra : rebase_source : 908fa43d5ac738a6c353d74475cb1910f6a318e8

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

fundamental revision of big operators on sets

locales for abstract orders

stepwise instantiation is more modular

added simp rule

more explicit code equations

tuned proofs

tuned simpset

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

tuned proofs

tune proofs

tune simpset for Complete_Lattices

added syntactic classes for "inf" and "sup"

move legacy candiates to bottom; marked candidates for default simp rules

more on complement

tuned notation

bot comes before top, inf before sup etc.

nice syntax for lattice INFI, SUPR;
various *_apply rules for lattice operations on fun;
more default simplification rules

primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`

dropped superfluous [code del]s

tuned whitespace

locale predicates of classes carry a mandatory "class" prefix

add bounded_lattice_bot and bounded_lattice_top type classes

add/change some lemmas about lattices

fixed typo

distributed theory Algebras to theories Groups and Lattices

Tuned interpretation proofs.

tuned import order

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

dropped mk_left_commute; use interpretation of locale abel_semigroup instead

killed a few warnings

tuned lattices theory fragements; generlized some lemmas from sets to lattices

moved lemmas about sup on bool to Lattices.thy

tuned proofs

be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer

some lemmas about strict order in lattices

proper class syntax for sublocale class < expr

Turned "x <= y ==> sup x y = y" (and relatives) into simp rules

localized interpretation of min/max-lattice

refinement of lattice classes

removed outdated comment

added boolean_algebra type class; tuned lattice duals

interpretation/interpret: prefixes are mandatory by default;

moved complete_lattice to Set.thy

dropped ID

migrated class package to new locale implementation

Conversion of HOL-Main and ZF to new locales.

tuned unfold_locales invocation

sup_bot and inf_top

new classes "top" and "bot"

`code func` now just `code`

added class preorder

- Now imports Fun rather than Orderings
- Moved "Set as lattice" section behind "Fun as lattice" section, since
sets are just functions.
- The instantiations
instantiation set :: (type) distrib_lattice
instantiation set :: (type) complete_lattice
are no longer needed, and the former definitions inf_set_eq, sup_set_eq,
Inf_set_def, and Sup_set_def can now be derived from abstract properties
of sup, inf, etc.

tuned proofs

dual orders and dual lattices

adjustions to due to instance target

dropped implicit assumption proof

tuned specifications of 'notation';

localized monotonicity; tuned syntax

antisymmetry not a default intro rule any longer

global class syntax

further localization

Simplified proofs due to transitivity reasoner setup.

mono_Int/Un: proper proof, avoid illegal schematic type vars;
removed obsolete ML bindings;

Sup now explicit parameter of complete_lattice

tuned

using class target

simplified HOL bootstrap

tuned proofs: avoid implicit prems;

rudimentary class target implementation

no special treatment in naming of locale predicates stemming form classes

tuned

tuned

dropped legacy ML bindings

integrated with LOrder.thy

stepping towards uniform lattice theory development in HOL

prefix of class interpretation not mandatory any longer

simplified proofs

tuned ML setup;

renamed locale partial_order to order

renaming

Modified lattice locale

stripped some legacy bindings

reworking of min/max lemmas

started reorgnization of lattice theories

renamed Lattice_Locales to Lattices