Fri, 04 Jan 2013 19:00:49 +0100 blanchet updated docs
Fri, 04 Jan 2013 19:00:49 +0100 blanchet renamed "kill" subcommand to avoid clash with "kill" keyword (which confuses Proof General and results in strange syntax highlighting)
Fri, 04 Jan 2013 19:00:49 +0100 blanchet tweaked fudge factor
Fri, 04 Jan 2013 13:03:21 +0100 wenzelm more NEWS;
Fri, 04 Jan 2013 12:44:47 +0100 wenzelm document 'locale_deps';
Fri, 04 Jan 2013 12:33:25 +0100 wenzelm prefer old graph browser in Isabelle/jEdit, which still produces better layout;
Fri, 04 Jan 2013 11:21:31 +0100 wenzelm more formal inlining of system information;
Fri, 04 Jan 2013 11:07:39 +0100 wenzelm tuned message -- suppress inlined system information;
Fri, 04 Jan 2013 01:39:32 +0100 smolkas merged
Thu, 03 Jan 2013 15:05:48 +0100 smolkas tuned
Thu, 03 Jan 2013 23:00:32 +0100 wenzelm avoid long enumeration of HO unifiers;
Thu, 03 Jan 2013 22:12:18 +0100 wenzelm disable search dialog pool on all platforms -- to prevent GUI synchronization problems seen on KDE (e.g. Kubuntu 12.10);
Thu, 03 Jan 2013 21:23:14 +0100 wenzelm merged
Thu, 03 Jan 2013 20:42:18 +0100 wenzelm maintain session index on Scala side, for more determistic results;
Thu, 03 Jan 2013 17:40:36 +0100 blanchet close formulas in the natural order, not its reverse -- so that Skolem arguments appear in the right order in Isar proofs
Thu, 03 Jan 2013 17:28:55 +0100 blanchet use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
Thu, 03 Jan 2013 17:10:12 +0100 blanchet rename variable in binder, not just in body
Thu, 03 Jan 2013 15:13:11 +0100 blanchet swap Vampire's Skolem arguments to bring them in line with what E and metis's new skolemizer do (helps Isar proof reconstruction in some cases)
Thu, 03 Jan 2013 14:41:05 +0100 blanchet tuned comment
Thu, 03 Jan 2013 14:23:10 +0100 wenzelm NEWS: ML runtime statistics;
Thu, 03 Jan 2013 14:12:12 +0100 wenzelm merged
Thu, 03 Jan 2013 14:10:57 +0100 wenzelm more interesting fields;
Thu, 03 Jan 2013 14:03:44 +0100 wenzelm always enable Future.ML_statistics where this makes sense -- runtime overhead should be negligible;
Thu, 03 Jan 2013 13:54:45 +0100 wenzelm improved Monitor_Dockable, based on ML_Statistics operations;
Thu, 03 Jan 2013 13:28:37 +0100 blanchet get rid of two-year-old hack, now that the "metis" skolemizer no longer gets stuck in HO unification
Thu, 03 Jan 2013 13:11:04 +0100 blanchet avoid explosion in higher-order unification algorithm
Thu, 03 Jan 2013 09:56:39 +0100 blanchet avoid repeated calls to metis from "resolve_tac" in case of ultimate failure
Thu, 03 Jan 2013 00:02:15 +0100 blanchet tuned comment
Wed, 02 Jan 2013 22:16:16 +0100 wenzelm merged
Wed, 02 Jan 2013 21:55:57 +0100 wenzelm added standard_frames convenience;
Wed, 02 Jan 2013 21:39:54 +0100 wenzelm some grouping of standard fields;
Wed, 02 Jan 2013 21:02:47 +0100 wenzelm some support for chart drawing;
Wed, 02 Jan 2013 19:23:18 +0100 wenzelm some support for ML statistics content interpretation;
Wed, 02 Jan 2013 18:03:38 +0100 wenzelm moved files;
Wed, 02 Jan 2013 17:58:53 +0100 wenzelm moved files;
Wed, 02 Jan 2013 16:48:22 +0100 wenzelm ML runtime statistics: read properties from build log;
Wed, 02 Jan 2013 15:08:38 +0100 wenzelm support File.read_gzip as well, in accordance to File.write_gzip;
Wed, 02 Jan 2013 13:50:59 +0100 wenzelm inline ML statistics into build log;
Wed, 02 Jan 2013 13:20:10 +0100 wenzelm removed outdated comment;
Wed, 02 Jan 2013 13:06:54 +0100 wenzelm enable Z3 for full test (cf. 6f48853f08d5);
Wed, 02 Jan 2013 20:53:01 +0100 smolkas removed old, unused code
Wed, 02 Jan 2013 20:52:39 +0100 smolkas removed whitespace
Wed, 02 Jan 2013 20:52:32 +0100 smolkas removed duplicate code
Wed, 02 Jan 2013 20:35:49 +0100 smolkas use rpair to avoid swap
Wed, 02 Jan 2013 19:59:06 +0100 blanchet generate "obtain" steps corresponding to skolemization inferences
Wed, 02 Jan 2013 16:32:40 +0100 blanchet keep E's and Vampire's skolemization steps
Wed, 02 Jan 2013 16:02:33 +0100 blanchet tuning
Wed, 02 Jan 2013 15:54:38 +0100 blanchet fixed oversensitive Skolem handling (cf. eaa540986291)
Wed, 02 Jan 2013 15:44:00 +0100 blanchet added "obtain" to Isar proof construction data structure
Wed, 02 Jan 2013 13:31:13 +0100 blanchet tuning
Wed, 02 Jan 2013 13:14:47 +0100 blanchet properly take the existential closure of skolems
Wed, 02 Jan 2013 10:54:36 +0100 blanchet use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
Wed, 02 Jan 2013 10:41:53 +0100 blanchet tuning
Wed, 02 Jan 2013 09:42:57 +0100 blanchet added 112 to list of known Z3 error codes
Wed, 02 Jan 2013 09:31:25 +0100 blanchet actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
Wed, 02 Jan 2013 09:13:50 +0100 blanchet added missing certificate file to "ROOT"
Tue, 01 Jan 2013 21:55:46 +0100 wenzelm more robust report_status: tolerate ML_statistics even if ignored right now, e.g. in batch build;
Tue, 01 Jan 2013 13:37:37 +0100 wenzelm more liberal edit_control_style: include preceeding control symbol to reduce potential for user surprise;
Tue, 01 Jan 2013 11:36:30 +0100 blanchet regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
Tue, 01 Jan 2013 11:35:22 +0100 blanchet Z3's soft timeout is expressed in ms, not in s -- this explains the frequenty "error code 112" failures we had recently
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip