NEWS
2015-11-02 wenzelm 2015-11-02 clarified completion of Isabelle symbols within document source;
2015-10-31 wenzelm 2015-10-31 back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
2015-10-27 paulson 2015-10-27 Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-24 wenzelm 2015-10-24 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
2015-10-21 wenzelm 2015-10-21 rendering for \<^verbatim>;
2015-10-21 wenzelm 2015-10-21 proper spaces around @{text};
2015-10-20 wenzelm 2015-10-20 added isabelle update_cartouches option -t;
2015-10-20 wenzelm 2015-10-20 another antiquotation short form: undecorated cartouche as alias for @{text}; document antiquotation @{text} ignores option "source";
2015-10-19 wenzelm 2015-10-19 tuned English;
2015-10-19 wenzelm 2015-10-19 added action "isabelle-emph"; changed shortcut of action "isabelle-reset";
2015-10-18 wenzelm 2015-10-18 clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;
2015-10-18 wenzelm 2015-10-18 support control symbol antiquotations;
2015-10-17 wenzelm 2015-10-17 added 'paragraph', 'subparagraph';
2015-10-17 wenzelm 2015-10-17 more explicit output of list items;
2015-10-14 wenzelm 2015-10-14 clarified control symbols;
2015-10-13 paulson 2015-10-13 new material on path_component_sets, inside, outside, etc. And more default simprules
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