2010-10-06 blanchet 2010-10-06 merged
2010-10-05 blanchet 2010-10-05 document latest changes to Meson/Metis/Sledgehammer
2010-10-04 haftmann 2010-10-04 turned distinct and sorted into inductive predicates: yields nice induction principles for free
2010-10-01 haftmann 2010-10-01 constant `contents` renamed to `the_elem`
2010-09-28 haftmann 2010-09-28 NEWS
2010-09-28 krauss 2010-09-28 no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.
2010-09-24 wenzelm 2010-09-24 clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees; tuned;
2010-09-23 haftmann 2010-09-23 CONTRIBUTORS and NEWS
2010-09-22 wenzelm 2010-09-22 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-17 wenzelm 2010-09-17 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
2010-09-13 haftmann 2010-09-13 merged
2010-09-13 haftmann 2010-09-13 'class' and 'type' are now antiquoations by default
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;