NEWS
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-12 wenzelm 2015-10-12 some control symbols for markup and formatting;
2015-10-10 wenzelm 2015-10-10 prefer symbols;
2015-10-09 wenzelm 2015-10-09 NEWS;
2015-10-09 kuncar 2015-10-09 NEWS
2015-10-06 blanchet 2015-10-06 news
2015-10-06 wenzelm 2015-10-06 added 'proposition' command;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-10-05 blanchet 2015-10-05 avoid too aggressive optimization of 'finite' predicate
2015-10-05 blanchet 2015-10-05 avoid unsound simplification of (C (s x)) when s is a selector but not C's
2015-10-03 blanchet 2015-10-03 speed up MaSh
2015-10-02 blanchet 2015-10-02 updated docs and NEWS
2015-10-02 wenzelm 2015-10-02 avoid useless empty case_names;
2015-09-30 wenzelm 2015-09-30 renamed jvmpath to platform_path;
2015-09-25 wenzelm 2015-09-25 merged
2015-09-25 wenzelm 2015-09-25 documentation for "Semantic subtype definitions"; misc tuning and simplification;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-22 wenzelm 2015-09-22 separate command 'print_definitions';
2015-09-22 haftmann 2015-09-22 tuned
2015-09-22 haftmann 2015-09-22 effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level
2015-09-21 wenzelm 2015-09-21 clarified isabelle.update-state;
2015-09-21 wenzelm 2015-09-21 added isabelle update_then;
2015-09-21 wenzelm 2015-09-21 NEWS;
2015-09-19 wenzelm 2015-09-19 NEWS;
2015-09-15 lammich 2015-09-15 Omega_Words_Fun: Infinite words as functions from nat.
2015-09-14 wenzelm 2015-09-14 replacement character for spaces;
2015-09-14 wenzelm 2015-09-14 single-instance application, even on Linux;
2015-09-14 wenzelm 2015-09-14 added isabelle jedit_client;
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-11 wenzelm 2015-09-11 convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
2015-09-10 haftmann 2015-09-10 dropped redundant NEWS
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-09 wenzelm 2015-09-09 eliminated \<Colon> from syntax of constraints;
2015-09-08 wenzelm 2015-09-08 clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
2015-09-08 wenzelm 2015-09-08 clarified Java runtime options for 32 vs. 64 bit;
2015-09-06 haftmann 2015-09-06 obsolete: if case_prod is fully applied, it is printed as proper case expression; eta-contracted variants are read best as "uncurry" combinator
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-09-06 wenzelm 2015-09-06 do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
2015-09-06 wenzelm 2015-09-06 removed obsolete theory Legacy_Mrec;
2015-09-06 wenzelm 2015-09-06 NEWS;
2015-08-31 wenzelm 2015-08-31 support x86_64-windows;
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);