NEWS
2015-08-31 wenzelm 2015-08-31 prefer symbols;
2015-08-28 blanchet 2015-08-28 eliminated obsolete environment variable
2015-08-27 blanchet 2015-08-27 robust handling of Vampire 4 proofs
2015-08-27 blanchet 2015-08-27 reverted 6ac3172985d4 -- the old URL has been restored
2015-08-21 wenzelm 2015-08-21 updated to jdk-8u60, with support for x86_64-windows;
2015-08-20 wenzelm 2015-08-20 tuned;
2015-08-20 wenzelm 2015-08-20 NEWS;
2015-08-20 wenzelm 2015-08-20 updated to polyml-5.5.3-20150820, with native x86-windows support;
2015-08-13 traytel 2015-08-13 tuned NEWS
2015-08-12 traytel 2015-08-12 NEWS, CONTRIBUTORS, documentation for lift_bnf
2015-08-08 haftmann 2015-08-08 direct bootstrap of integer division from natural division
2015-08-04 wenzelm 2015-08-04 eliminated clone;
2015-07-28 paulson 2015-07-28 the Cauchy integral theorem and related material
2015-07-27 wenzelm 2015-07-27 NEWS;
2015-07-26 wenzelm 2015-07-26 eliminated atac, rtac, etac, dtac, ftac;
2015-07-12 Lars Hupel 2015-07-12 Quickcheck setup for finite sets
2015-07-09 wenzelm 2015-07-09 SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
2015-07-08 haftmann 2015-07-08 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-07-02 wenzelm 2015-07-02 documentation for 'subgoal' command;
2015-07-01 wenzelm 2015-07-01 tuned;
2015-06-30 wenzelm 2015-06-30 renamed "default" to "standard", to make semantically clear what it is;
2015-06-30 wenzelm 2015-06-30 tuned;
2015-06-29 wenzelm 2015-06-29 improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-06-27 wenzelm 2015-06-27 premises in 'show' are treated like 'assume';
2015-06-26 blanchet 2015-06-26 updated SystemOnTPTP URL
2015-06-25 wenzelm 2015-06-25 implicit goal cases are legacy;
2015-06-25 wenzelm 2015-06-25 added method "goals" for proper subgoal cases;
2015-06-24 wenzelm 2015-06-24 clarified 'case' command;
2015-06-22 wenzelm 2015-06-22 support 'when' statement, which corresponds to 'presume';
2015-06-22 wenzelm 2015-06-22 added method "sleep";
2015-06-22 wenzelm 2015-06-22 clarified nesting of Isar goal structure; tuned message;
2015-06-19 wenzelm 2015-06-19 merged
2015-06-19 wenzelm 2015-06-19 discontinued unused 'defer_recdef';
2015-06-19 haftmann 2015-06-19 separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
2015-06-19 haftmann 2015-06-19 generalized some theorems about integral domains and moved to HOL theories
2015-06-19 nipkow 2015-06-19 renamed multiset_of -> mset
2015-06-18 nipkow 2015-06-18 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