NEWS
2015-03-31 haftmann 2015-03-31 NEWS
2015-03-30 wenzelm 2015-03-30 clarified NEWS (cf. 97872c658a44);
2015-03-29 wenzelm 2015-03-29 rule_insts_schematic is considered legacy and false by default;
2015-03-23 haftmann 2015-03-23 explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation
2015-03-25 blanchet 2015-03-25 more multiset theorems
2015-03-25 wenzelm 2015-03-25 NEWS;
2015-03-24 wenzelm 2015-03-24 admit dummy patterns in instantiations; clarified context;
2015-03-23 wenzelm 2015-03-23 NEWS;
2015-03-19 paulson 2015-03-19 New material for complex sin, cos, tan, Ln, also some reorganisation
2015-03-18 paulson 2015-03-18 new HOL Light material about exp, sin, cos
2015-03-18 noschinl 2015-03-18 added proof method rewrite
2015-03-17 paulson 2015-03-17 Merge
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-10 blanchet 2015-03-10 documented renamed theories
2015-03-09 wenzelm 2015-03-09 merged
2015-03-09 wenzelm 2015-03-09 support structural composition (THEN_ALL_NEW) for proof methods; clarified preparation for goal restriction: Goal.conjunction_tac only once; export Method.parse0, notably for Eisbach; more explicit type cases_state;
2015-03-09 paulson 2015-03-09 Removed the infix operator "choose" to allow HOLCF to build
2015-03-07 wenzelm 2015-03-07 NEWS;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 nipkow 2015-03-04 merged
2015-03-04 nipkow 2015-03-04 Removed the obsolete functions "natfloor" and "natceiling"
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-28 haftmann 2015-02-28 spelling
2015-02-27 wenzelm 2015-02-27 tuned whitespace;
2015-02-23 wenzelm 2015-02-23 Goal.prove_multi is superseded by the fully general Goal.prove_common;
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-18 haftmann 2015-02-18 eliminated fact duplicates
2015-02-14 haftmann 2015-02-14 dropped redundancy
2015-02-11 blanchet 2015-02-11 updated NEWS
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-02-05 haftmann 2015-02-05 dropped obsolete external entrance point
2015-01-26 wenzelm 2015-01-26 NEWS;
2015-01-25 wenzelm 2015-01-25 discontinued obsolete option "document_graph";
2015-01-13 hoelzl 2015-01-13 NEWS
2015-01-06 wenzelm 2015-01-06 NEWS;
2015-01-01 boehmes 2015-01-01 merged
2015-01-01 boehmes 2015-01-01 updated NEWS
2014-12-30 wenzelm 2014-12-30 added system property isabelle.laf, notably for initial system dialog; let L&F take care of font scaling, e.g. GTK+ for Linux where X11 dpi scaling does not really work;
2014-12-30 wenzelm 2014-12-30 NEWS;
2014-12-22 wenzelm 2014-12-22 discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
2014-12-22 wenzelm 2014-12-22 system option "pretty_margin" is superseded by "thy_output_margin";
2014-12-12 wenzelm 2014-12-12 Synchronized.value is actually synchronized (NB: underlying Unsynchronized.ref is not necessarily volatile);
2014-12-08 wenzelm 2014-12-08 expand ML cartouches to Input.source; tuned signature;
2014-12-08 haftmann 2014-12-08 NEWS
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-26 wenzelm 2014-11-26 added ML antiquotation @{apply n} or @{apply n(k)};
2014-11-24 blanchet 2014-11-24 updated NEWS
2014-11-13 wenzelm 2014-11-13 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
2014-11-12 immler 2014-11-12 NEWS
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-02 wenzelm 2014-11-02 added update_header tool;
2014-11-02 wenzelm 2014-11-02 uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;
2014-11-01 wenzelm 2014-11-01 command-line terminator ";" is no longer accepted;
2014-10-31 wenzelm 2014-10-31 discontinued Isar TTY loop;
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-10-28 wenzelm 2014-10-28 'notepad' requires proper nesting of begin/end;
2014-10-26 wenzelm 2014-10-26 clarified default;