NEWS
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-13 nipkow 2010-09-13 added and renamed lemmas
2010-09-10 wenzelm 2010-09-10 merged
2010-09-09 bulwahn 2010-09-09 changing String.literal to a type instead of a datatype
2010-09-09 wenzelm 2010-09-09 NEWS: some notes on interrupts;
2010-09-08 haftmann 2010-09-08 NEWS
2010-09-07 nipkow 2010-09-07 renamed expand_*_eq in HOLCF as well
2010-09-06 wenzelm 2010-09-06 ML_Context.thm and ML_Context.thms no longer pervasive;
2010-09-06 wenzelm 2010-09-06 merged;
2010-09-05 krauss 2010-09-05 removed duplicate lemma
2010-09-05 wenzelm 2010-09-05 turned show_brackets into proper configuration option; Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-03 wenzelm 2010-09-03 turned eta_contract into proper configuration option;
2010-09-03 wenzelm 2010-09-03 configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
2010-09-03 wenzelm 2010-09-03 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
2010-09-03 wenzelm 2010-09-03 merged
2010-09-02 hoelzl 2010-09-02 merged
2010-09-02 hoelzl 2010-09-02 NEWS
2010-09-03 wenzelm 2010-09-03 turned show_consts into proper configuration option;
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;