Mon, 29 Jul 2013 14:43:21 +0200 wenzelm back to model.update_perspective with delay (cf. a20631db9c8a);
Mon, 29 Jul 2013 14:37:59 +0200 wenzelm show displaced messages (e.g. from protocol thread) as raw output;
Mon, 29 Jul 2013 14:18:57 +0200 wenzelm actually purge removed goal futures -- avoid memory leak;
Mon, 29 Jul 2013 13:43:43 +0200 wenzelm tuned -- less redundant data structure;
Mon, 29 Jul 2013 13:43:12 +0200 wenzelm always init GUI state;
Mon, 29 Jul 2013 13:28:27 +0200 wenzelm tuned signature;
Mon, 29 Jul 2013 13:24:15 +0200 wenzelm discontinued notion of "stable" result -- running execution is never canceled;
Mon, 29 Jul 2013 13:00:36 +0200 wenzelm obsolete;
Mon, 29 Jul 2013 12:50:16 +0200 wenzelm support declarative editor_execution_range, instead of old-style check/cancel buttons;
Mon, 29 Jul 2013 18:06:39 +0200 blanchet avoid duplicating Var when the types do not quite fit -- since this step occurs before type inference
Mon, 29 Jul 2013 17:27:56 +0200 blanchet updated Sledgehammer prover versions
Mon, 29 Jul 2013 16:13:35 +0200 blanchet parse nonnumeric identifiers in E proofs correctly
Mon, 29 Jul 2013 15:42:04 +0200 blanchet simplified Vampire hack -- no need to run it for other ATPs
Mon, 29 Jul 2013 15:30:31 +0200 blanchet added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
Sun, 28 Jul 2013 20:51:15 +0200 wenzelm prefer examples that work out of the box;
Sun, 28 Jul 2013 20:50:44 +0200 wenzelm breakable @{file};
Sun, 28 Jul 2013 20:10:59 +0200 wenzelm prefer existing swipl;
Sun, 28 Jul 2013 20:10:21 +0200 wenzelm avoid machine running batch process for months;
Sun, 28 Jul 2013 12:59:59 +0200 traytel more converse(p) theorems; tuned proofs;
Sat, 27 Jul 2013 22:44:04 +0200 wenzelm more uniform cleanup;
Sat, 27 Jul 2013 22:38:06 +0200 wenzelm tuned;
Sat, 27 Jul 2013 22:20:25 +0200 wenzelm discontinued historic document formats;
Sat, 27 Jul 2013 22:16:04 +0200 wenzelm avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
Sat, 27 Jul 2013 21:50:30 +0200 wenzelm tuned;
Sat, 27 Jul 2013 21:43:12 +0200 wenzelm discontinued ISABELLE_DOC_FORMAT;
Sat, 27 Jul 2013 21:21:47 +0200 wenzelm more direct inclusion of tikz pictures;
Sat, 27 Jul 2013 21:10:18 +0200 wenzelm obsolete;
Sat, 27 Jul 2013 21:01:35 +0200 wenzelm documentation is always in PDF;
Sat, 27 Jul 2013 20:28:28 +0200 wenzelm merged;
Sat, 27 Jul 2013 20:27:25 +0200 wenzelm clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;
Sat, 27 Jul 2013 17:34:56 +0200 wenzelm clarified meaning of options for "isabelle options";
Sat, 27 Jul 2013 18:02:41 +0200 haftmann more correct context for dynamic invocations of static code conversions etc.
Sat, 27 Jul 2013 16:59:25 +0200 wenzelm support isabelle options -g;
Sat, 27 Jul 2013 16:44:58 +0200 wenzelm tuned spelling;
Sat, 27 Jul 2013 16:44:40 +0200 wenzelm tuned;
Sat, 27 Jul 2013 16:35:51 +0200 wenzelm standardized aliases;
Thu, 25 Jul 2013 16:46:53 +0200 traytel transfer rule for {c,d}tor_{,un}fold
Thu, 25 Jul 2013 12:25:07 +0200 traytel two useful relation theorems
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Wed, 24 Jul 2013 17:15:59 +0200 krauss derive specialized version of full fixpoint induction (with admissibility)
Wed, 24 Jul 2013 15:29:23 +0200 krauss export mono_thm
Wed, 24 Jul 2013 22:54:47 +0200 nipkow merged Def_Init_Sound_X into Def_Init_X
Wed, 24 Jul 2013 13:03:53 +0200 traytel proper transfer rule format for map_transfer
Wed, 24 Jul 2013 07:39:37 +0200 krauss merged
Tue, 23 Jul 2013 16:56:46 +0200 krauss eliminate duplicate calls when moving to closed form -- graph decomposition chokes on duplicates
Tue, 23 Jul 2013 18:36:23 +0200 boehmes removed obsolete HOL-Boogie session;
Tue, 23 Jul 2013 13:14:14 +0200 traytel transfer stored bnf theorems into the "current" theory when retrieving a bnf (avoids non-trivial merges)
Tue, 23 Jul 2013 13:10:27 +0200 traytel separate ML interface to note facts of a bnf
Mon, 22 Jul 2013 21:12:15 +0200 traytel transfer rule for map (not yet registered as a transfer rule)
Sun, 21 Jul 2013 14:02:33 +0200 nipkow tuned exercises
Sat, 20 Jul 2013 16:45:00 +0200 wenzelm clarified option name, with improved sort order wrt. "time" options;
Sat, 20 Jul 2013 16:29:06 +0200 wenzelm document update at high priority -- important;
Sat, 20 Jul 2013 16:27:55 +0200 wenzelm option editor_execution_priority;
Sat, 20 Jul 2013 16:18:17 +0200 wenzelm obscure options;
Sat, 20 Jul 2013 16:16:23 +0200 wenzelm print_state at high priority -- fast and important;
Fri, 19 Jul 2013 23:29:43 +0200 wenzelm proper Future.shutdown, to wait for the scheduler thread to finish remaining tasks (notably external processes);
Fri, 19 Jul 2013 20:56:39 +0200 wenzelm old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483);
Fri, 19 Jul 2013 17:58:57 +0200 wenzelm just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
Fri, 19 Jul 2013 17:35:12 +0200 wenzelm turned pattern unify flag into configuration option (global only);
Fri, 19 Jul 2013 16:36:13 +0200 traytel merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip