NEWS
Mon, 17 Feb 2014 22:39:20 +0100 wenzelm subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOL-IMP);
Mon, 17 Feb 2014 14:07:26 +0100 wenzelm NEWS;
Mon, 17 Feb 2014 13:31:42 +0100 blanchet updated NEWS
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'rel_option' into 'option_rel'
Sun, 16 Feb 2014 21:33:28 +0100 blanchet folded 'list_all2' with the relator generated by 'datatype_new'
Sun, 16 Feb 2014 18:39:41 +0100 blanchet more NEWS
Wed, 12 Feb 2014 10:20:31 +0100 blanchet [mq]: news
Mon, 10 Feb 2014 22:08:18 +0100 wenzelm discontinued axiomatic 'classes', 'classrel', 'arities';
Tue, 04 Feb 2014 09:04:59 +0000 Lars Hupel interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Tue, 04 Feb 2014 01:35:48 +0100 blanchet removed legacy 'metisFT' method
Mon, 03 Feb 2014 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
Mon, 03 Feb 2014 17:18:38 +0100 blanchet added new option to documentation
Thu, 30 Jan 2014 14:37:53 +0100 blanchet renamed Sledgehammer options for symmetry between positive and negative versions
Sun, 26 Jan 2014 14:01:19 +0100 wenzelm discontinued obsolete attribute "standard";
Sat, 25 Jan 2014 22:06:07 +0100 wenzelm explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
Sat, 25 Jan 2014 16:59:41 +0100 wenzelm NEWS for 31afce809794;
Wed, 22 Jan 2014 23:51:26 +0100 wenzelm NEWS;
Wed, 22 Jan 2014 17:14:27 +0100 wenzelm merged
Wed, 22 Jan 2014 15:10:33 +0100 wenzelm inner syntax token language allows regular quoted strings;
Tue, 21 Jan 2014 13:51:10 +0100 blanchet updated NEWS
Sun, 19 Jan 2014 22:38:17 +0100 boehmes removed obsolete remote_cvc3 and remote_z3
Fri, 17 Jan 2014 20:20:20 +0100 wenzelm clarified @{rail} syntax: prefer explicit \<newline> symbol;
Wed, 15 Jan 2014 23:25:28 +0100 wenzelm added \<newline> symbol, which is used for char/string literals in HOL;
Mon, 13 Jan 2014 20:20:44 +0100 wenzelm activation of Z3 via "z3_non_commercial" system option (without requiring restart);
Mon, 13 Jan 2014 18:47:48 +0100 wenzelm tuned;
Sun, 12 Jan 2014 18:40:49 +0100 wenzelm NEWS;
Wed, 01 Jan 2014 12:57:26 +0100 wenzelm avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Mon, 30 Dec 2013 20:35:17 +0100 wenzelm added system option "jedit_print_mode";
Wed, 25 Dec 2013 17:39:07 +0100 haftmann abolished slightly odd global lattice interpretation for min/max
Mon, 23 Dec 2013 16:16:36 +0100 haftmann NEWS
Tue, 17 Dec 2013 11:12:10 +0100 immler NEWS
Sun, 15 Dec 2013 15:10:16 +0100 haftmann disambiguation of interpretation prefixes
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Thu, 12 Dec 2013 22:56:28 +0100 wenzelm discontinued legacy_isub_isup;
Mon, 09 Dec 2013 22:49:27 +0100 haftmann NEWS
Mon, 09 Dec 2013 20:16:12 +0100 wenzelm provide @{file_unchecked} in Isabelle/Pure;
Mon, 09 Dec 2013 12:16:52 +0100 wenzelm added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
Fri, 06 Dec 2013 23:36:28 +0100 wenzelm NEWS;
Fri, 06 Dec 2013 22:10:45 +0100 wenzelm clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
Thu, 05 Dec 2013 18:02:55 +0100 wenzelm relocate NEWS to post-release version (cf. 7a14f831d02d);
Thu, 05 Dec 2013 17:58:03 +0100 wenzelm merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
Sun, 01 Dec 2013 17:09:35 +0100 wenzelm tuned;
Sat, 30 Nov 2013 17:26:00 +0100 wenzelm NEWS;
Mon, 25 Nov 2013 21:36:10 +0100 wenzelm NEWS;
Thu, 21 Nov 2013 22:13:11 +0100 wenzelm NEWS;
Wed, 20 Nov 2013 23:00:18 +0100 wenzelm updated to Isabelle2013-2;
Thu, 05 Dec 2013 13:22:00 +0100 blanchet make sure acyclicity axiom gets generated in the case where the problem involves mutually recursive datatypes
Thu, 05 Dec 2013 09:23:59 +0100 Andreas Lochbihler news
Tue, 26 Nov 2013 09:49:52 +0100 traytel NEWS
Mon, 25 Nov 2013 18:18:58 +0100 haftmann even more precise NEWS
Wed, 20 Nov 2013 17:00:49 +0100 wenzelm NEWS;
Tue, 19 Nov 2013 18:14:56 +0100 haftmann more correct NEWS
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Sat, 16 Nov 2013 17:39:11 +0100 wenzelm toplevel function "use" refers to raw ML bootstrap environment;
Mon, 11 Nov 2013 17:44:21 +0100 wenzelm merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;
Sat, 09 Nov 2013 11:24:21 +0100 wenzelm tuned whitespace;
Tue, 05 Nov 2013 18:16:16 +0100 wenzelm no default shortcut for isabelle.reset-font-size -- avoid conflict with unsplit-current;
Wed, 30 Oct 2013 17:05:23 +0100 wenzelm more on file-system access;
Mon, 14 Oct 2013 15:21:45 +0200 wenzelm tuned;
less more (0) -1000 -300 -100 -60 tip