allow arbitrary enumerations of basis in locale for generation of borel sets

repaired slip accidentally introduced in 57209cfbf16b

prefer implementation in HOL; n.b. code_reflect cannot reflect type synonyms

corrected headers

hide constants of auxiliary type finmap

generalized to copy of countable types instead of instantiation of nat for discrete topology

added projective limit; proof is based on auxiliary type finmap::polish_space

regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards

tuned -- eliminated obsolete citation of isabelle-ref;

updated basic equality rules;

removed somewhat pointless historic material;

updated unification options;

removed some historic material that is obsolete or rarely used;

tuned;

updated section on ordered rewriting;

updated subgoaler/solver/looper;

removed somewhat pointless historic material; tuned;

tuned;

updated explanation of rewrite rules;

(re)moved old material about Simplifier;

some coverage of "resolution without lifting", which should be normally avoided;

removed somewhat pointless historic material;

updated biresolve_tac, bimatch_tac; removed obscure historical material;

moved classical wrappers to IsarRef; removed somewhat pointless historic material;

avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");

updated citations;

tuned;

removed junk;

removed pointless historic material;

more on Simplifier rules, based on old material;

refurbished Simplifier examples;

more on the Simplifier, based on old material;

more concise/precise documentation;

tuned text

replaced relation by function - simplifies development

made SMLNJ happier

import Sublist rather than PrefixOrder to avoid unnecessary class instantiation

prefer explicit Random.seed

dropped dead code

tuned import order

tuned layout

fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies

create temp directory if not already created

merged

new theory IMP/Finite_Reachable

avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit

centralized term printing code

thread context correctly when printing backquoted facts

dropped dead code; tuned theory text

modernized, simplified and compacted oracle and proof method glue code; corrected slips with poly.Pw and Orderings.less(_eq)

merged

fixed underscores

moved lemmas into projective_family; added header for theory Projective_Family

removed redundant/unnecessary assumptions from projective_family

assume probability spaces; allow empty index set

added projective_family; generalized generator in product_prob_space to projective_family

moved lemmas further up

tuned proofs

using hyp_subst_tac that allows to pass the current simpset to avoid the renamed bound variable warning in the simplifier

hyp_subst_tac allows to pass an optional simpset to the internal simplifier call to avoid renamed bound variable warnings in the simplifier call