NEWS
Sat, 19 Sep 2015 21:09:38 +0200 wenzelm NEWS;
Tue, 15 Sep 2015 11:18:25 +0200 lammich Omega_Words_Fun: Infinite words as functions from nat.
Mon, 14 Sep 2015 17:39:29 +0200 wenzelm replacement character for spaces;
Mon, 14 Sep 2015 16:44:09 +0200 wenzelm single-instance application, even on Linux;
Mon, 14 Sep 2015 16:06:32 +0200 wenzelm added isabelle jedit_client;
Sun, 13 Sep 2015 20:20:16 +0200 wenzelm renamed method "goals" to "goal_cases" to emphasize its meaning;
Fri, 11 Sep 2015 17:57:34 +0200 wenzelm convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
Thu, 10 Sep 2015 11:59:12 +0200 haftmann dropped redundant NEWS
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Wed, 09 Sep 2015 14:47:41 +0200 wenzelm eliminated \<Colon> from syntax of constraints;
Tue, 08 Sep 2015 17:34:46 +0200 wenzelm clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
Tue, 08 Sep 2015 15:37:13 +0200 wenzelm clarified Java runtime options for 32 vs. 64 bit;
Sun, 06 Sep 2015 22:14:51 +0200 haftmann obsolete: if case_prod is fully applied, it is printed as proper case expression;
Sun, 06 Sep 2015 22:14:51 +0200 haftmann prefer "uncurry" as canonical name for case distinction on products in combinatorial view
Sun, 06 Sep 2015 21:55:13 +0200 wenzelm do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
Sun, 06 Sep 2015 14:51:49 +0200 wenzelm removed obsolete theory Legacy_Mrec;
Sun, 06 Sep 2015 13:37:18 +0200 wenzelm NEWS;
Mon, 31 Aug 2015 22:45:40 +0200 wenzelm support x86_64-windows;
Mon, 31 Aug 2015 21:01:21 +0200 wenzelm prefer symbols;
Fri, 28 Aug 2015 16:48:05 +0200 blanchet eliminated obsolete environment variable
Thu, 27 Aug 2015 20:16:07 +0200 blanchet robust handling of Vampire 4 proofs
Thu, 27 Aug 2015 20:10:40 +0200 blanchet reverted 6ac3172985d4 -- the old URL has been restored
Fri, 21 Aug 2015 16:47:57 +0200 wenzelm updated to jdk-8u60, with support for x86_64-windows;
Thu, 20 Aug 2015 17:39:07 +0200 wenzelm tuned;
Thu, 20 Aug 2015 14:31:09 +0200 wenzelm NEWS;
Thu, 20 Aug 2015 14:13:00 +0200 wenzelm updated to polyml-5.5.3-20150820, with native x86-windows support;
Thu, 13 Aug 2015 11:14:16 +0200 traytel tuned NEWS
Wed, 12 Aug 2015 20:46:33 +0200 traytel NEWS, CONTRIBUTORS, documentation for lift_bnf
Sat, 08 Aug 2015 10:51:33 +0200 haftmann direct bootstrap of integer division from natural division
Tue, 04 Aug 2015 23:11:16 +0200 wenzelm eliminated clone;
Tue, 28 Jul 2015 16:16:13 +0100 paulson the Cauchy integral theorem and related material
Mon, 27 Jul 2015 17:56:08 +0200 wenzelm NEWS;
Sun, 26 Jul 2015 22:26:11 +0200 wenzelm eliminated atac, rtac, etac, dtac, ftac;
Sun, 12 Jul 2015 13:04:42 +0200 Lars Hupel Quickcheck setup for finite sets
Thu, 09 Jul 2015 22:36:31 +0200 wenzelm SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
Wed, 08 Jul 2015 14:01:41 +0200 haftmann avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Thu, 02 Jul 2015 14:09:43 +0200 wenzelm documentation for 'subgoal' command;
Wed, 01 Jul 2015 10:53:14 +0200 wenzelm tuned;
Tue, 30 Jun 2015 15:20:56 +0200 wenzelm renamed "default" to "standard", to make semantically clear what it is;
Tue, 30 Jun 2015 10:40:42 +0200 wenzelm tuned;
Mon, 29 Jun 2015 20:55:46 +0200 wenzelm improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
Sat, 27 Jun 2015 00:10:24 +0200 wenzelm premises in 'show' are treated like 'assume';
Fri, 26 Jun 2015 11:08:33 +0200 blanchet updated SystemOnTPTP URL
Thu, 25 Jun 2015 23:49:05 +0200 wenzelm implicit goal cases are legacy;
Thu, 25 Jun 2015 21:45:00 +0200 wenzelm added method "goals" for proper subgoal cases;
Wed, 24 Jun 2015 21:26:03 +0200 wenzelm clarified 'case' command;
Mon, 22 Jun 2015 20:36:33 +0200 wenzelm support 'when' statement, which corresponds to 'presume';
Mon, 22 Jun 2015 19:22:48 +0200 wenzelm added method "sleep";
Mon, 22 Jun 2015 16:48:27 +0200 wenzelm clarified nesting of Isar goal structure;
Fri, 19 Jun 2015 21:33:03 +0200 wenzelm merged
Fri, 19 Jun 2015 20:14:50 +0200 wenzelm discontinued unused 'defer_recdef';
Fri, 19 Jun 2015 07:53:35 +0200 haftmann separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
Fri, 19 Jun 2015 07:53:33 +0200 haftmann generalized some theorems about integral domains and moved to HOL theories
Fri, 19 Jun 2015 15:55:22 +0200 nipkow renamed multiset_of -> mset
Thu, 18 Jun 2015 16:17:51 +0200 nipkow NEWS
Wed, 17 Jun 2015 17:33:22 +0200 nipkow NEWS
Mon, 15 Jun 2015 16:59:27 +0200 wenzelm vacuous fact `TERM x`;
Mon, 15 Jun 2015 00:23:18 +0200 wenzelm tuned whitespace;
Sun, 14 Jun 2015 23:22:08 +0200 wenzelm improved treatment of Element.Obtains via Expression.prepare_stmt;
less more (0) -1000 -300 -100 -60 tip