NEWS
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-28 haftmann 2010-08-28 merged
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-27 wenzelm 2010-08-27 merged
2010-08-27 haftmann 2010-08-27 merged
2010-08-27 haftmann 2010-08-27 official support for Scala
2010-08-27 wenzelm 2010-08-27 structure Unsynchronized is never opened and set/reset/toggle have been discontinued; retain Unsynchronized.change alias for Proof General;
2010-08-27 wenzelm 2010-08-27 merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 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