NEWS
Sun, 04 May 2014 18:57:45 +0200 blanchet renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
Sun, 04 May 2014 18:53:58 +0200 blanchet added 'satx' proof method to Try0
Sun, 04 May 2014 18:14:58 +0200 blanchet renamed 'xxx_size' to 'size_xxx' for old datatype package
Sun, 04 May 2014 16:17:53 +0200 boehmes removed obsolete internal SAT solvers
Sat, 03 May 2014 22:47:43 +0200 wenzelm support for path completion based on file-system content;
Fri, 02 May 2014 23:31:25 +0200 wenzelm merged
Fri, 02 May 2014 23:30:47 +0200 wenzelm NEWS;
Fri, 02 May 2014 21:18:50 +0200 haftmann enforce case of identifiers only to accomodate strict language requirements (or clear separation of constructors from variables in the case of SML)
Thu, 01 May 2014 22:56:59 +0200 boehmes added internal proof-producing SAT solver
Thu, 01 May 2014 09:30:32 +0200 haftmann NEWS
Tue, 29 Apr 2014 15:42:19 +0200 wenzelm require explicit 'document_files';
Sat, 26 Apr 2014 22:57:51 +0200 wenzelm merged
Sat, 26 Apr 2014 22:51:21 +0200 wenzelm NEWS;
Sat, 26 Apr 2014 21:37:09 +1000 kleing retired wwwfind
Wed, 23 Apr 2014 10:23:27 +0200 blanchet updated NEWS
Sat, 19 Apr 2014 17:23:05 +0200 wenzelm added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
Tue, 15 Apr 2014 22:41:10 +0200 wenzelm more NEWS;
Tue, 15 Apr 2014 19:11:34 +0200 wenzelm clarified abbreviations for cartouche delimiters, to work in any context;
Tue, 15 Apr 2014 00:07:07 +0200 wenzelm NEWS;
Sat, 12 Apr 2014 21:58:58 +0200 wenzelm NEWS;
Fri, 11 Apr 2014 11:52:28 +0200 wenzelm explicit 'document_files' in session ROOT specifications;
Thu, 10 Apr 2014 10:30:32 +0200 wenzelm NEWS;
Wed, 09 Apr 2014 17:54:09 +0200 wenzelm allow text cartouches in regular outer syntax categories "text" and "altstring";
Mon, 07 Apr 2014 16:37:57 +0200 wenzelm refrain from changing jEdit default shortcuts, due to potential for conflicts and actually not working on Mac OS X;
Sun, 06 Apr 2014 16:59:41 +0200 wenzelm renamed "isabelle-process" to "isabelle_process", with shell function to avoid dynamic path lookups;
Fri, 04 Apr 2014 22:51:22 +0200 wenzelm support for jEdit Navigator plugin;
Fri, 04 Apr 2014 12:07:48 +0200 wenzelm added ML antiquotation @{print};
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Wed, 02 Apr 2014 18:35:01 +0200 hoelzl moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Mon, 31 Mar 2014 21:13:51 +0200 wenzelm cumulative NEWS;
Thu, 27 Mar 2014 17:12:40 +0100 wenzelm clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
Wed, 26 Mar 2014 08:59:53 +0100 wenzelm tuned;
Tue, 25 Mar 2014 19:03:02 +0100 wenzelm proper configuration option "ML_print_depth";
Tue, 25 Mar 2014 16:54:38 +0100 wenzelm clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
Tue, 25 Mar 2014 14:52:35 +0100 wenzelm some SML examples;
Tue, 25 Mar 2014 13:18:10 +0100 wenzelm added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
Mon, 24 Mar 2014 12:00:17 +0100 wenzelm discontinued Toplevel.debug in favour of system option "exception_trace";
Sat, 22 Mar 2014 08:37:43 +0100 haftmann generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Thu, 20 Mar 2014 22:00:13 +0100 wenzelm more static checking of proof methods;
Wed, 19 Mar 2014 18:47:22 +0100 haftmann elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
Wed, 19 Mar 2014 15:35:07 +0100 hoelzl NEWS
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
Tue, 18 Mar 2014 16:16:28 +0100 wenzelm clarified modules;
Sun, 16 Mar 2014 18:09:04 +0100 haftmann normalising simp rules for compound operators
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Fri, 14 Mar 2014 17:32:11 +0100 wenzelm merged
Thu, 13 Mar 2014 11:34:05 +0100 wenzelm added ML antiquotation @{path};
Fri, 14 Mar 2014 01:28:13 +0100 blanchet updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
Thu, 13 Mar 2014 08:56:08 +0100 haftmann dropped redundant theorems
Thu, 13 Mar 2014 07:07:07 +0100 nipkow enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
Wed, 12 Mar 2014 22:57:50 +0100 wenzelm tuned signature -- clarified module name;
Wed, 12 Mar 2014 22:44:55 +0100 wenzelm added ML antiquotation @{here};
Wed, 12 Mar 2014 21:58:48 +0100 wenzelm simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
Thu, 06 Mar 2014 22:15:01 +0100 wenzelm merged
Thu, 06 Mar 2014 21:33:15 +0100 wenzelm some NEWS;
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:29:18 +0100 blanchet renamed 'prod_rel' to 'rel_prod'
Thu, 06 Mar 2014 15:25:21 +0100 blanchet renamed 'sum_rel' to 'rel_sum'
less more (0) -1000 -300 -100 -60 tip