NEWS
2015-06-17 nipkow 2015-06-17 NEWS
2015-06-15 wenzelm 2015-06-15 vacuous fact `TERM x`;
2015-06-15 wenzelm 2015-06-15 tuned whitespace;
2015-06-14 wenzelm 2015-06-14 improved treatment of Element.Obtains via Expression.prepare_stmt; discontinued pointless all_types ctxt: prep_var is always sequential;
2015-06-13 wenzelm 2015-06-13 merged
2015-06-13 wenzelm 2015-06-13 more on 'consider' and related concepts;
2015-06-13 wenzelm 2015-06-13 implicit rule for method "cases";
2015-06-13 wenzelm 2015-06-13 renamed "prems" to "that";
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-10 wenzelm 2015-06-10 merged
2015-06-10 wenzelm 2015-06-10 support for "if prems" in local goal statements;
2015-06-09 wenzelm 2015-06-09 more uniform treatment of auto bindings vs. explicit user bindings; misc tuning;
2015-06-09 wenzelm 2015-06-09 allow for_fixes for 'have', 'show' etc.; tuned signature;
2015-06-09 wenzelm 2015-06-09 clarified abstracted term bindings (again, see c8384ff11711);
2015-06-10 fleury 2015-06-10 tuned
2015-06-10 Mathias Fleury 2015-06-10 tuned
2015-06-10 Mathias Fleury 2015-06-10 Renaming multiset operators < ~> <#,...
2015-06-08 wenzelm 2015-06-08 clarified abstracted term bindings;
2015-06-08 wenzelm 2015-06-08 more careful treatment of term bindings in 'obtain' proof body; tuned signature;
2015-06-05 wenzelm 2015-06-05 added Isar command 'supply';
2015-06-05 wenzelm 2015-06-05 tuned;
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-06-01 haftmann 2015-06-01 explicit argument expansion of uncheck rules; rewriting of user-space type system must behave similarly to abbreviations
2015-06-01 wenzelm 2015-06-01 discontinued legacy;
2015-05-29 blanchet 2015-05-29 removed model checks from Nitpick
2015-05-28 blanchet 2015-05-28 made Auto Sledgehammer behave more like the real thing
2015-05-25 wenzelm 2015-05-25 merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
2015-05-23 wenzelm 2015-05-23 clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
2015-05-17 wenzelm 2015-05-17 added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
2015-05-07 wenzelm 2015-05-07 use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
2015-05-05 wenzelm 2015-05-05 tuned;
2015-05-04 wenzelm 2015-05-04 tuned;
2015-05-04 kuncar 2015-05-04 NEWS
2015-05-04 nipkow 2015-05-04 no more simp_legacy_precond
2015-04-19 wenzelm 2015-04-19 back to post-release mode -- after fork point;
2015-04-17 wenzelm 2015-04-17 added Eisbach, using version 3752768caa17 of its Bitbucket repository;
2015-04-17 wenzelm 2015-04-17 tuned;
2015-04-17 wenzelm 2015-04-17 tuned for release;
2015-04-17 traytel 2015-04-17 (low importance) NEWS
2015-04-17 wenzelm 2015-04-17 allow to exclude session groups;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-16 wenzelm 2015-04-16 clarified thy_deps;
2015-04-16 wenzelm 2015-04-16 let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
2015-04-15 wenzelm 2015-04-15 NEWS;
2015-04-14 wenzelm 2015-04-14 NEWS;
2015-04-12 wenzelm 2015-04-12 tuned;
2015-04-11 paulson 2015-04-11 Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
2015-04-11 wenzelm 2015-04-11 tuned spelling;
2015-04-11 wenzelm 2015-04-11 misc tuning for release;
2015-04-10 wenzelm 2015-04-10 tuned;
2015-04-10 nipkow 2015-04-10 renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
2015-04-09 wenzelm 2015-04-09 merged
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-09 blanchet 2015-04-09 introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
2015-04-08 blanchet 2015-04-08 tuned wording
2015-04-08 blanchet 2015-04-08 Z3 news
2015-04-08 blanchet 2015-04-08 renamed multiset ordering to free up nice <# etc. symbols for the standard subset
2015-04-08 wenzelm 2015-04-08 misc tuning for release;
2015-04-07 nipkow 2015-04-07 Removed mcard because it is equal to size
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;