2012-11-19 ago hoelzl tuned: use induction rule sigma_sets_induct_disjoint
2012-11-19 ago hoelzl tuned FinMap
2012-11-19 ago hoelzl merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-19 ago wenzelm more refs;
2012-11-18 ago wenzelm isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
2012-11-18 ago wenzelm proper jvmpath for windows;
2012-11-18 ago wenzelm more generous tracing_limit, with explicit system option;
2012-11-18 ago wenzelm adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
2012-11-18 ago wenzelm update options via protocol;
2012-11-18 ago wenzelm more accurate pixel_range -- do not round offset here;
2012-11-18 ago wenzelm tuned signature;
2012-11-17 ago wenzelm prefer absolute default $USER_HOME/Scratch.thy;
2012-11-17 ago wenzelm more portable process exit;
2012-11-17 ago wenzelm tuned -- eliminate pointless ML method definition;
2012-11-17 ago wenzelm tuned;
2012-11-17 ago wenzelm NEWS;
2012-11-17 ago wenzelm tuned structure of Isabelle/HOL;
2012-11-17 ago wenzelm method setup for Classical steps;
2012-11-17 ago wenzelm tuned signature;
2012-11-17 ago wenzelm updated keywords;
2012-11-16 ago hoelzl moved (b)choice_iff(') to Hilbert_Choice
2012-11-16 ago hoelzl move theorems to be more generally useable
2012-11-16 ago wenzelm merged
2012-11-16 ago wenzelm made SML/NJ happy;
2012-11-16 ago hoelzl renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
2012-11-16 ago hoelzl renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
2012-11-16 ago hoelzl measurability for nat_case and comb_seq
2012-11-16 ago hoelzl rules for AE and prob
2012-11-16 ago hoelzl rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication
2012-11-16 ago hoelzl more measurability rules
2012-11-16 ago immler renamed to more appropriate lim_P for projective limit
2012-11-16 ago immler allow arbitrary enumerations of basis in locale for generation of borel sets
2012-11-15 ago haftmann repaired slip accidentally introduced in 57209cfbf16b
2012-11-15 ago haftmann prefer implementation in HOL;
2012-11-15 ago immler corrected headers
2012-11-15 ago immler hide constants of auxiliary type finmap
2012-11-15 ago immler generalized to copy of countable types instead of instantiation of nat for discrete topology
2012-11-15 ago immler added projective limit;
2012-11-15 ago immler regularity of measures, therefore:
2012-11-15 ago wenzelm tuned -- eliminated obsolete citation of isabelle-ref;
2012-11-12 ago wenzelm updated basic equality rules;
2012-11-12 ago wenzelm removed somewhat pointless historic material;
2012-11-11 ago wenzelm updated unification options;
2012-11-11 ago wenzelm removed some historic material that is obsolete or rarely used;
2012-11-11 ago wenzelm tuned;
2012-11-11 ago wenzelm updated section on ordered rewriting;
2012-11-10 ago wenzelm updated subgoaler/solver/looper;
2012-11-08 ago wenzelm removed somewhat pointless historic material;
2012-11-08 ago wenzelm tuned;
2012-11-08 ago wenzelm updated explanation of rewrite rules;
2012-11-07 ago wenzelm (re)moved old material about Simplifier;
2012-11-07 ago wenzelm some coverage of "resolution without lifting", which should be normally avoided;
2012-11-07 ago wenzelm removed somewhat pointless historic material;
2012-11-07 ago wenzelm updated biresolve_tac, bimatch_tac;
2012-11-07 ago wenzelm moved classical wrappers to IsarRef;
2012-11-04 ago wenzelm avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");
2012-11-04 ago wenzelm updated citations;
2012-11-04 ago wenzelm tuned;
2012-11-04 ago wenzelm removed junk;
2012-11-04 ago wenzelm removed pointless historic material;