lots of new material, ultimately related to measure theory

more symbols;

standardized towards new-style formal comments: isabelle update_comments;

line break before op was intentional

tuned notation

Manual updates towards conversion of "op" syntax

--HG--
extra : amend_source : fd689f9cef643a634d5ce2dfded9a17206473899

Restored correct spacing for set comprehensions

new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product

more symbols;

dedicated definition for coprimality

--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae

canonical introduction and destruction rules for pairwise

--HG--
extra : rebase_source : 4b2f35fa103369ed3a81ec56ba05c3a18d42b5e4

HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)

new material connected with HOL Light measure theory, plus more rationalisation

More mainly topological results

simple new lemmas, mostly about sets

misc tuning and modernization;

misc tuning and modernization;

tuned;

more theorems

misc tuning and modernization;

new results about topology

tuned proofs;

Lots of new material for multivariate analysis

Moved material from AFP/Randomised_Social_Choice to distribution

renamings and refinements

new theorems about convex hulls, etc.; also, renamed some theorems

Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results

old HOL syntax is for input only;

more canonical names

revisions to limits and derivatives, plus new lemmas

add the proof of the central limit theorem

--HG--
extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f
extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b

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

isabelle update_cartouches -c -t;

new lemmas about topology, etc., for Cauchy integral formula

discontinued specific HTML syntax;

New theorems about connected sets. And pairwise moved to Set.thy.

isabelle update_cartouches;

new simp rule

add lemmas

Not a simprule, as it complicates proofs

New lemmas and a bit of tidying up.

misc tuning;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

import general theorems from AFP/Markov_Models

proper context for assume_tac (atac remains as fall-back without context);

modernized header uniformly as section;

eliminated aliases;

tuned

--HG--
extra : rebase_source : ec19f13e8067586494f4cc6530970036992e80cd

tuned proofs

tuned;
elimination rule subset_imageE;
typical composition collapsing rewrite order in lemma image_image_eq_image_comp;
destruction rules ball_imageD, bex_imageD

A bit of tidying up

explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;

tuned signature;
clarified context;

killed most "no_atp", to make Sledgehammer more complete

added lemmas

syntax translations always depend on context;

simplifier uses proper Proof.context instead of historic type simpset;

modifiers for classical wrappers operate on Proof.context instead of claset;

extended set comprehension notation with {pttrn : A . P}

more lemmas about intervals

Sieve of Eratosthenes

made element and subset relations non-associative (just like all orderings)

rename Set.project to Set.filter - more appropriate name

more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

tuned

tuned simpset

beautified

removing unnecessary premise from diff_single_insert

eliminated obsolete aliases;

massaging of code setup for sets

--HG--
extra : rebase_source : d88e8eabd9d4067b161ff0d4e077408f826712f8

incorporated various theorems from theory More_Set into corpus

--HG--
extra : rebase_source : 3382b66ad31349cb7368f064c467aa4a53845dd2

tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);

interaction of set operations for execution and membership predicate

--HG--
extra : rebase_source : 88e19fdc682e81ad835b4c75d2758a6cba48e84a

cleanup of code declarations

--HG--
extra : rebase_source : 7376929a640011e27309be6654ccf370df37e60a

fundamental theorems on Set.bind

--HG--
extra : rebase_source : f60f78a12efe9f4496619a04d48afb38f7eccb9d

semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat

--HG--
extra : rebase_source : 7ed52e71daa69142f147737027b94acaef451223

moved various set operations to theory Set (resp. Product_Type)

`set` is now a proper type constructor; added operation for set monad

tuned signature;

just one data slot per module;
tuned;

modernized some old-style infix operations, which were left over from the time of ML proof scripts;

eliminated obsolete "standard";

hide not_member as also member

Set.thy: remove redundant [simp] declarations

added new lemmas

lemma Compl_insert: "- insert x A = (-A) - {x}"

modernized signature of Term.absfree/absdummy;
eliminated obsolete Term.list_abs_free;

more coherent structure in and across theories

moved lemmas to appropriate theory

moving UNIV = ... equations to their proper theories

tuned lemma positions and proofs

misc tuning and simplification;

proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;

modernized Quantifier1 simproc setup;

discontinued special treatment of structure Mixfix;
eliminated slightly odd no_syn convenience;

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

renewing specifications in HOL: replacing types by type_synonym

moved most fundamental lemmas upwards

bot comes before top, inf before sup etc.

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

Move SUP_commute, SUP_less_iff to HOL image;
Cleanup generic complete_lattice lemmas in Positive_Infinite_Real;
Cleanup lemma positive_integral_alt;

Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

constant `contents` renamed to `the_elem`

renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI

put expand_(fun/set)_eq back in as synonyms, for compatibility

expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets

formerly unnamed infix equality now named HOL.eq

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

formerly unnamed infix impliciation now named HOL.implies

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

"no_atp" fact that leads to unsound proofs

"no_atp" a few facts that often lead to unsound proofs

dropped superfluous [code del]s

qualified constants Set.member and Set.Collect

qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

use lattice theorems to prove set theorems

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

Added vimage_inter_cong

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

Changed 'bounded unique existential quantifiers' from a constant to syntax translation.

new theory Algebras.thy for generic algebraic structures

killed a few warnings

Removed eq_to_mono2, added not_mono.

New theory Probability/Borel.thy, and some associated lemmas

dropped redundant gen_ prefix

Some new lemmas concerning sets

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

Removal of the unused atpset concept, the atp attribute and some related code.

tuned proofs

inter and union are mere abbreviations for inf and sup

tuned the simp rules for Int involving insert and intervals.

Set.UNIV and Set.empty are mere abbreviations for top and bot

moved complete_lattice &c. into separate theory

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

set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice

attempt for more concise setup of non-etacontracting binders

Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy

swapped bootstrap order of UNION/Union and INTER/Inter in theory Set

less digestible

refined outline structure

closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text

more antiquotations;

refinement of lattice classes

added boolean_algebra type class; tuned lattice duals

structure Thm: less pervasive names;

authentic syntax for Pow and image

finite lemmas

insert now qualified and with authentic syntax

fine-tuned elimination of comprehensions involving x=t.

"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".

tuned;

tuned some theorem and attribute bindings

reverted to old version of Set.thy -- strange effects have to be traced first

restructured theory Set.thy

set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

finiteness lemmas

Added strong congruence rule for UN.

`code func` now just `code`

rudimentary code setup for set operations

remove simp attribute from range_composition

removed some dubious code lemmas

- Now uses Orderings as parent theory
- "'a set" is now just a type abbreviation for "'a => bool"
- The instantiation "set :: (type) ord" and the definition of (p)subset is
no longer needed, since it is subsumed by the order on functions and booleans.
The derived theorems (p)subset_eq can be used as a replacement.
- mem_Collect_eq and Collect_mem_eq can now be derived from the definitions
of mem and Collect.
- Replaced the instantiation "set :: (type) minus" by the two instantiations
"fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq
can be used as a replacement for the definition set_diff_def
- Replaced the instantiation "set :: (type) uminus" by the two instantiations
"fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq
can be used as a replacement for the definition Compl_def.
- Variable P in rule split_if must be instantiated manually in proof of
split_if_mem2 due to problems with HO unification
- Moved definition of dense linear orders and proofs about LEAST from
Orderings to Set
- Deleted code setup for sets

constant HOL.eq now qualified

explicit class "eq" for operational equality

replaced 'ML_setup' by 'ML';

eliminated change_claset/simpset;

moved some set lemmas from Set.thy here

improved code theorem setup

splitted class uminus from class minus

adjustions to due to instance target

instance command as rudimentary class target

interpretation of typedecls: instantiation to class type

avoid name clashes when generating code for union, inter

added lemmas

convenient obtain rule for sets

clarified code lemmas

made sets executable

Made UN_Un simp

dropped junk

ATP blacklisting is now in theory data, attribute noatp

updated code generator setup

simplified HOL bootstrap

code lemma for contents

changed code generator invocation syntax

Isar definitions are now added explicitly to code theorem table

fixed typo

added instance of sets as distributive lattices

syntax: proper body priorty for derived binders;

tuned ML setup;

some new lemmas

tuned ML setup;

dropped FIXME comment

fixed syntax for bounded quantification

removed legacy ML bindings;

restructured some proofs

updated (binder) syntax/notation;

more robust syntax for definition/abbreviation/notation;

moved transitivity rules to Orderings.thy

dropped LOrder dependency

image_constant_conv no longer [simp]

started reorgnization of lattice theories

renamed 'const_syntax' to 'notation';

simplified code generator setup

linear arithmetic splits certain operators (e.g. min, max, abs)

new results

tuned concrete syntax -- abbreviation/const_syntax;

reactivated translations for less/less_eq;

refined 'abbreviation';

Converted translations to abbbreviations.
Removed a few odd functions from Map and AssocList.
Moved chg_map from Map to Bali/Basis.

subsetI is often necessary

renamed op < <= to Orderings.less(_eq)

renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

subset_refl now included using the atp attribute

adaptions to codegen_package

declare 'defn' rules;

*** empty log message ***

removed or modified some instances of [iff]

new lemmas

removed obsolete/unused setup_induction;

simprocs: static evaluation of simpset;

restoring the old status of subset_refl

duplicate axioms in ATP linkup, and general fixes

change_claset/simpset;
Simplifier.inherit_context instead of Simplifier.inherit_bounds;

Term.absdummy;

a name for empty_not_insert

more finalconsts;

renamed rules to iprover

tuned theory dependencies;

more simprules now have names

classical rules must have names for ATP integration

simprocs: Simplifier.inherit_bounds;

tweaked

Added strong_ball_cong and strong_bex_cong (these are now the standard
congruence rules for Ball and Bex).

Added thms by Brian Huffmann

integrated Jeremy's FiniteLib

tuning

Moved oderings from HOL into the new Orderings.thy

Modified locales: improved implementation of "includes".

import -> imports

New theory header syntax.

undid UN/INT syntax

new simprules Int_subset_iff and Un_subset_iff

Merged in license change from Isabelle2004

\<^bsub>/\<^esub> syntax: unbreakable block;

new theorem Collect_imp_eq

Corrected printer bug for bounded quantifiers Q x<=y. P

lemma disjoint_int_union removed - too special

New simp rules added:

insert_disjoint
disjoint_insert
disjoint_int_union

improved subscript syntax;

use more symbols in HTML output

Various changes to HOL-Algebra;
Locale instantiation.

streamlined treatment of quotients for the integers

Efficient, graph-based reasoner for linear and partial orders.
+ Setup as solver in the HOL simplifier.

Modified UN and INT xsymbol syntax: made index subscript

conversion of Real/PReal to Isar script;
type "complex" is now in class "field"

*** empty log message ***

misc tidying

added rev_ballE

moved one proof, added another

new UN/INT simprules

*** empty log message ***

new lemma

Undid eta change for UN/INT.

new theorem Compl_partition2

removed some problems with print translations

added print translations tha avoid eta contraction for important binders.

Added a few thms about UN/INT/{}/UNIV

added the new elim rule psubsetE

removal of blast.overloaded

sane interface for simprocs;

simplified locale predicates;

rev_bexI [intro?];

Added insert_disjoint and disjoint_insert [simp], and simplified proofs

clarified syntax of ``long'' statements: fixes/assumes/shows;

converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);

tuned ``syntax (output)'';

renamed class "term" to "type" (actually "HOL.type");

theory Inverse_Image converted and moved to Set;

eliminated old "symbols" syntax, use "xsymbols" instead;

tuned;

theory Calculation move to Set;

lemma Least_mono moved from Typedef.thy to Set.thy;

converted theory "Set";

removed Ord;

fixed set comprehension print translation

`` -> and ``` -> ``

range declared as syntax;

fixed \<Union>, \<Inter> syntax;

beautified spacing for binders with symbols syntax, analogous to HOL.thy

new-style infix declaration for "image"

a little tidying; also FIXED BAD TYPE in INTER1, UNION1

replaced HOL_quantifiers flag by "HOL" print mode;
simplified HOL basic syntax (more orthogonal);

Finally removing "Compl" from HOL

Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed

From Compl(A) to -A

Removal of "disjoint" translation

fixed disjount translation;

Minor tidying up.

added caveat

UNIV now a constant; UNION1, INTER1 now translations and no longer have
separate rules for themselves

adapted typed_print_translation;

adapted to qualified names;

fixed dots;

fixed infix syntax;

Overloading of "^" requires new type class "power", with types "nat" and
"set" in that class. The operator itself is declared in Nat.thy

Distributed Psubset stuff to basic set theory files, incl Finite.
Added stuff by bu.

improved translations for subset symbols syntax: constraints;

moved inj and surj from Set to Fun and Inv -> inv.

added proper subset symbols syntax;

fixed \<subseteq> input;

adaptions for symbol font

added set inclusion symbol syntax;

fixed alternative quantifier symbol syntax;

fixed pris of binder syntax;

added "op :", "op ~:" syntax;
added symbols syntax;

New infix syntax: breaks line BEFORE operator

Corrected associativity: must be to right, as the type dictatess

Redefining "range" as a macro

*** empty log message ***

repaired critical proofs depending on the order inside non-confluent SimpSets,
(temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"

Added a constant UNIV == {x.True}
Added many new rewrite rules for sets.
Moved LEAST into Nat.
Added cardinality to Finite.

removed quotes from types in consts and syntax sections

added 8bit pragmas

HOL.thy:

"@" is no longer introduced as a "binder" but has its own explicit
translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further
translation rules for abstractions with patterns take care of the rest. This
is very modular and avoids problems with "binders" such as "!" mentioned
below.

let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u)


Set.thy:

UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@"
above, except that "@" was a "binder" originally.


Prod.thy:

Added new syntax for pttrn which allows arbitrarily nested tuples. Two
translation rules take care of %pttrn. Unfortunately they cannot be
reversed. Hence a little ML-code is used as well.

Note that now "! (x,y). ..." is syntactically valid but leads to a
translation error. This is because "!" is introduced as a "binder" which
means that its translation into lambda-terms is not done by a rewrite rule
(aka macro) but by some fixed ML-code which comes after the rewriting stage
and does not know how to handle patterns. This looks like a minor blemish
since patterns in unbounded quantifiers are not that useful (well, except
maybe in unique existence ...). Ideally, there should be two syntactic
categories:

idts, as we know and love it, which does not admit patterns.
patterns, which is what idts has become now.

There is one more point where patterns are now allowed but don't make sense:

{e | idts . P}

where idts is the list of local variables.


Univ.thy: converted the defs for <++> and <**> into pattern form. It worked
perfectly.

new version of HOL with curried function application