tidied up a few little proofs

moved subset_image_inj into Hilbert_Choice

The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale

more specific keyword kinds;

avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default

proper congruence rule for image operator

--HG--
extra : rebase_source : 71f59936260619419f4d3f7f86d1b930bc771065

isabelle update -u path_cartouches;

isabelle update -u control_cartouches;

tuned proof text

tuned proof

clarified status of legacy input abbreviations

A few new results, elimination of duplicates and more use of "pairwise"

some modernization of notation

--HG--
extra : rebase_source : 5e9836a69d8e9ea3e5e173b956099f5a132a6d8b

moved lemmas

Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)

--HG--
extra : amend_source : fa78190ac2ee02ba33d22a4ee58362bc893ff097

Changes to complete distributive lattices due to Viorel Preoteasa

lots of new material, ultimately related to measure theory

more symbols;

removed GreatestM

introduced arg_max

removed LeastM; is now arg_min

added lemma

restructured matter on polynomials and normalized fractions

--HG--
extra : rebase_source : 71508900ff150d54097ae5c4c2da7176f09cb625

tuned proofs;

Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);

clarified obscure facts;

tuned proof;

tuned;

misc tuning and modernization;

tuned proofs -- avoid unstructured calculation;

dedicated locale for total bijections

more theorems

eliminated old 'def';
tuned comments;

clarified rule structure;

old HOL syntax is for input only;

prefer abbreviations for compound operators INFIMUM and SUPREMUM

removed subsumed dependency

isabelle update_cartouches -c -t;

prod_case as canonical name for product type eliminator

eliminated \<Colon>;

standardized some occurences of ancient "split" alias

--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5

New material and fixes related to the forthcoming Stone-Weierstrass development

isabelle update_cartouches;

tuned whitespace;

cleaned up mess

--HG--
extra : rebase_source : 04297756c04f5c420a600bfcff8ddda6c3e3a82d

import general theorems from AFP/Markov_Models

modernized header uniformly as section;

made 'moura' tactic more powerful

renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods

moved skolem method

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

--HG--
extra : rebase_source : 8664c1d86ed72607199cc8197a480070514ae330

moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

tuned

--HG--
extra : rebase_source : ec19f13e8067586494f4cc6530970036992e80cd

more simp rules for Fun.swap

removed unused 'ax_specification', to give 'specification' a chance to become localized;
tuned whitespace;

load Metis a little later

renamed 'nat_{case,rec}' to '{case,rec}_nat'

moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'

dissolved 'Fun_More_FP' (a BNF dependency)

more algebraic terminology for theories about big operators

eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main

qualifed popular user space names

syntax translations always depend on context;

moved (b)choice_iff(') to Hilbert_Choice

--HG--
extra : rebase_source : 7b26a1d119d233fe8974def95c9d33bf40c710fa

moved quite generic material from theory Enum to more appropriate places

--HG--
extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9

consolidated names of theorems on composition;
generalized former theorem UN_o;
comp_assoc orients to the right, as is more common

prefer ML_file over old uses;

tuned proofs;

declare command keywords via theory header, including strict checking outside Pure;

eliminated obsolete "standard";

tuned proofs

new fastforce replacing fastsimp - less confusing name

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

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

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

Replace surj by abbreviation; remove surj_on.

got rid of overkill "meson_choice" attribute;
tuning

remove Meson from Hilbert_Choice

added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice

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

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

use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
this *really* speeds up things -- HOL now builds 12% faster on my machine

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

get rid of many duplicate simp rule warnings

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

inv_onto -> inv_into

added inv_def for compatibility as a lemma

Inv -> inv_onto, inv abbr. inv_onto UNIV.

discontinued ancient tradition to suffix certain ML module names with "_package"

--HG--
rename : src/HOL/Import/import_package.ML => src/HOL/Import/import.ML
rename : src/HOL/Nominal/nominal_package.ML => src/HOL/Nominal/nominal.ML
rename : src/HOL/Tools/specification_package.ML => src/HOL/Tools/choice_specification.ML
rename : src/HOL/Tools/datatype_package/datatype_package.ML => src/HOL/Tools/datatype_package/datatype.ML
rename : src/HOL/Tools/function_package/fundef_package.ML => src/HOL/Tools/function_package/fundef.ML
rename : src/HOL/Tools/inductive_package.ML => src/HOL/Tools/inductive.ML
rename : src/HOL/Tools/inductive_set_package.ML => src/HOL/Tools/inductive_set.ML
rename : src/HOL/Tools/old_primrec_package.ML => src/HOL/Tools/old_primrec.ML
rename : src/HOL/Tools/primrec_package.ML => src/HOL/Tools/primrec.ML
rename : src/HOL/Tools/recdef_package.ML => src/HOL/Tools/recdef.ML
rename : src/HOL/Tools/record_package.ML => src/HOL/Tools/record.ML
rename : src/HOL/Tools/typecopy_package.ML => src/HOL/Tools/typecopy.ML
rename : src/HOL/Tools/typedef_package.ML => src/HOL/Tools/typedef.ML

dropped legacy ML bindings; tuned

added/moved lemmas by Andreas Lochbihler

Plain, Main form meeting points in import hierarchy

added lemma

Merged theories about wellfoundedness into one: Wellfounded.thy

* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.

tuned proofs

moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
added some

<= and < on nat no longer depend on wellfounded relations

added lemmas

replaced axioms/finalconsts by proper axiomatization;

improvements to proof reconstruction. Some files loaded in a different order

removed theory NatArith (now part of Nat);

Adapted to changes in FixedPoint theory.

removal of functional reflexivity axioms

added lemma exE_some (from specification_package.ML);

more finalconsts;

comment

generlization of some "nat" theorems

meson method taking an argument list

migrated theory headers to new format

converted some induct_tac to induct

import -> imports

New theory header syntax.

improved symbolic syntax of Eps: \<some> for mode "epsilon";

conversion of Hilbert_Choice to Isar script

New lemmas about inversion of restricted functions.
HOL-Algebra: new locale "ring" for non-commutative rings.

misc tidying

Added package for definition by specification.

removed some problems with print translations

added print translations tha avoid eta contraction for important binders.

Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"

tuned declarations;

tuned;
meson lemmas from Tools/meson.ML;

tuned;

avoid ML bindings;

Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice

partial restructuring to reduce dependence on Axiom of Choice