2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-19 huffman 2010-11-19 merged
2010-11-17 huffman 2010-11-17 accumulated NEWS updates for HOLCF
2010-11-18 blanchet 2010-11-18 mention Sledgehammer with SMT
2010-11-17 boehmes 2010-11-17 require the b2i file ending in the boogie_open command (for consistency with the theory header)
2010-11-08 boehmes 2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-06 krauss 2010-11-06 abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-11-05 wenzelm 2010-11-05 moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
2010-11-04 haftmann 2010-11-04 merged
2010-11-03 haftmann 2010-11-03 Theory Multiset provides stable quicksort implementation of sort_key.
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-11-03 wenzelm 2010-11-03 discontinued obsolete function sys_error and exception SYS_ERROR;
2010-10-31 nipkow 2010-10-31 merged
2010-10-29 nipkow 2010-10-29 Plus -> Sum_Type.Plus
2010-10-30 wenzelm 2010-10-30 support for real valued preferences;
2010-10-30 wenzelm 2010-10-30 support for real valued configuration options;
2010-10-29 wenzelm 2010-10-29 merged
2010-10-29 bulwahn 2010-10-29 NEWS
2010-10-28 wenzelm 2010-10-28 discontinued obsolete ML antiquotation @{theory_ref};
2010-10-26 krauss 2010-10-26 fixed typo
2010-10-26 krauss 2010-10-26 NEWS
2010-10-26 boehmes 2010-10-26 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
2010-10-25 wenzelm 2010-10-25 merged
2010-10-25 wenzelm 2010-10-25 significantly improved Isabelle/Isar implementation manual;
2010-10-25 blanchet 2010-10-25 merged
2010-10-25 blanchet 2010-10-25 introduced manual version of "Auto Solve" as "solve_direct"
2010-10-25 wenzelm 2010-10-25 added ML antiquotation @{assert};
2010-10-24 nipkow 2010-10-24 renamed nat_number
2010-10-22 blanchet 2010-10-22 make Sledgehammer minimizer fully work with SMT
2010-10-21 blanchet 2010-10-21 use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
2010-10-14 krauss 2010-10-14 NEWS
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