NEWS
2010-08-27 wenzelm 2010-08-27 proper context for various Thy_Output options, via official configuration options in ML and Isar;
2010-08-25 wenzelm 2010-08-25 discontinued obsolete 'global' and 'local' commands;
2010-08-23 hoelzl 2010-08-23 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.
2010-08-23 haftmann 2010-08-23 dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-08-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions
2010-08-19 wenzelm 2010-08-19 merged
2010-08-19 haftmann 2010-08-19 deglobalized named HOL constants
2010-08-18 haftmann 2010-08-18 merged
2010-08-18 haftmann 2010-08-18 NEWS
2010-08-18 haftmann 2010-08-18 more helpful NEWS entry
2010-08-17 haftmann 2010-08-17 preemptive NEWS
2010-08-18 haftmann 2010-08-18 NEWS
2010-08-18 haftmann 2010-08-18 deglobalization
2010-08-17 wenzelm 2010-08-17 discontinued support for Poly/ML 5.0 and 5.1 versions;
2010-08-17 haftmann 2010-08-17 NEWS and CONTRIBUTORS
2010-08-11 haftmann 2010-08-11 NEWS
2010-08-03 wenzelm 2010-08-03 theory loading: only the master source file is looked-up in the implicit load path;
2010-07-31 ballarin 2010-07-31 Documentation of 'interpret' updated.
2010-07-22 wenzelm 2010-07-22 discontinued special treatment of ML files -- no longer complete extensions on demand; simplified Thy_Load.check_file, with uniform error reporting; added Thy_Load.test_file for non-strict checking; misc tuning and simplification;
2010-07-21 wenzelm 2010-07-21 ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);
2010-07-14 haftmann 2010-07-14 export_code without file prints to standard output
2010-07-07 bulwahn 2010-07-07 added NEWS entry
2010-07-02 haftmann 2010-07-02 fixed spelling
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
2010-07-01 hoelzl 2010-07-01 Updated NEWS
2010-06-29 haftmann 2010-06-29 merged
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem; refined code generation operations in List.thy
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-25 wenzelm 2010-06-25 explicit treatment of UTF8 sequences as Isabelle symbols;
2010-06-21 wenzelm 2010-06-21 merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;
2010-06-15 haftmann 2010-06-15 added code_simp infrastructure
2010-06-15 haftmann 2010-06-15 merged
2010-06-14 haftmann 2010-06-14 NEWS
2010-06-14 haftmann 2010-06-14 removed simplifier congruence rule of "prod_case"
2010-06-10 haftmann 2010-06-10 qualified type "*"; qualified constants Pair, fst, snd, split
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-06-07 wenzelm 2010-06-07 back to non-release mode;
2010-06-21 wenzelm 2010-06-21 final tuning;
2010-06-11 wenzelm 2010-06-11 NEWS: IsabelleText font;
2010-06-07 berghofe 2010-06-07 Documented changes in induct, cases, and nominal_induct method.
2010-06-07 wenzelm 2010-06-07 more NEWS;
2010-06-07 wenzelm 2010-06-07 more NEWS; tuned;
2010-06-04 krauss 2010-06-04 NEWS (more strict internal axioms/defs format)
2010-06-04 wenzelm 2010-06-04 spelling;
2010-06-03 wenzelm 2010-06-03 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
2010-06-03 krauss 2010-06-03 clarified
2010-06-03 krauss 2010-06-03 mention unconstrain in NEWS
2010-06-02 wenzelm 2010-06-02 improved parallelism of proof term normalization;
2010-06-01 blanchet 2010-06-01 merged
2010-06-01 blanchet 2010-06-01 update NEWS
2010-06-01 blanchet 2010-06-01 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-06-01 blanchet 2010-06-01 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-05-31 wenzelm 2010-05-31 notes on Isabelle/jEdit;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-27 wenzelm 2010-05-27 merged
2010-05-27 boehmes 2010-05-27 merged
2010-05-27 boehmes 2010-05-27 moved SMT into the HOL image
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 misc updates for release;