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

fixes for Free_Abelian_Groups

new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map

some renamings and a bit of new material

isabelle update -u control_cartouches;

new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml

more lemmas

de-applying and simplification

tuned headers;

move FuncSet back to HOL-Library (amending 493b818e8e10)

--HG--
rename : src/HOL/FuncSet.thy => src/HOL/Library/FuncSet.thy

more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);

prefer main entry points of HOL;

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

removed some old ASCII syntax;

more symbols via abbrevs;

eliminated use of empty "assms";

some uses of 'obtain' with structure statement;

more canonical names

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

isabelle update_cartouches -c -t;

prefer symbols;

discontinued specific HTML syntax;

cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution

--HG--
extra : rebase_source : cffce7b3e322f3c274d9117a0dfdd311d4ba66a1

import general thms from Density_Compiler

--HG--
extra : rebase_source : 48a3b47f755d8099564008b93076eae81453a674

modernized header;

tuned whitespace;
more symbols;

add Giry monad

--HG--
extra : rebase_source : 3ceb1c0fa2e24cb05e37856566255a7b56f80af7

tuned;

add restrict_space measure

tuned proofs -- less guessing;

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

merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

--HG--
extra : rebase_source : e65af8d29763871aedf04aed10bdeb869effca0b

move theorems to be more generally useable

--HG--
extra : rebase_source : c1c0d1f5576f4d469d1b4618663774e2f297a214

moved lemmas to appropriate places

reduced warnings;

adding extensional function spaces to the FuncSet library theory

new lemmas

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

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

--HG--
rename : src/HOL/Probability/Lebesgue.thy => src/HOL/Probability/Lebesgue_Integration.thy

New theory Probability, which contains a development of measure theory

inv_onto -> inv_into

Inv -> inv_onto, inv abbr. inv_onto UNIV.

lemma funcset_id by Jeremy Avigad

fixed name

tuned FuncSet

tuned

Made Pi_I [simp]

Main is (Complex_Main) base entry point in library theories

arbitrary is undefined

absolute imports of HOL/*.thy theories

established Plain theory and image

removed obsolete skolem declarations -- done by Theory.at_end;

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

more robust syntax for definition/abbreviation/notation;

renamed 'const_syntax' to 'notation';

fixed translations: CONST;

skolem declarations for built-in theorems

tuned;

tuned concrete syntax -- abbreviation/const_syntax;

replaced syntax/translations by abbreviation;

print_translation: does not handle _idtdummy;

import -> imports

New theory header syntax.

more on bij_betw

new bij_betw operator

new lemmas

tuned document;

use more symbols in HTML output

Proof tidying

Tidied. New Pi-theorem.

new theory for Pi-sets, restrict, etc.