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
Fri, 19 Jul 2013 14:51:45 +0200 traytel permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
Fri, 19 Jul 2013 15:48:04 +0200 nipkow added exerciese
Fri, 19 Jul 2013 12:00:31 +0200 traytel do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
Thu, 18 Jul 2013 23:13:44 +0200 wenzelm modify background theory where it is actually required (cf. 51dfdcd88e84);
Thu, 18 Jul 2013 22:32:00 +0200 wenzelm tuned messages -- avoid text folds stemming from Pretty.chunks;
Thu, 18 Jul 2013 22:18:20 +0200 wenzelm proper system options for 'find_theorems';
Thu, 18 Jul 2013 22:00:35 +0200 wenzelm guard unify tracing via visible status of global theory;
Thu, 18 Jul 2013 21:57:27 +0200 wenzelm provide global operations as well;
Thu, 18 Jul 2013 21:20:09 +0200 wenzelm tuned signature;
Thu, 18 Jul 2013 21:06:21 +0200 wenzelm tuned;
Thu, 18 Jul 2013 20:53:22 +0200 wenzelm explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
Thu, 18 Jul 2013 13:12:54 +0200 wenzelm immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
Wed, 17 Jul 2013 23:51:10 +0200 wenzelm merged
Wed, 17 Jul 2013 23:33:16 +0200 wenzelm tuned message;
Wed, 17 Jul 2013 23:32:28 +0200 wenzelm tuned signature;
Wed, 17 Jul 2013 23:36:33 +0200 smolkas tuned
Wed, 17 Jul 2013 21:48:21 +0200 wenzelm merged
Wed, 17 Jul 2013 21:25:27 +0200 wenzelm more opportunistic string_of_clause, to make double-sure its Syntax.string_of_term uncheck phase does not crash, and thus bomb ambiguous input via failed composition of warning (e.g. HOL/Imperative_HOL/ex/Linked_List.thy: lemma merge_simps);
Wed, 17 Jul 2013 21:04:38 +0200 wenzelm tuned spelling;
Wed, 17 Jul 2013 12:41:59 +0900 Christian Sternagel show variants in error messages; more precise error messages (give witnesses for multiple instances)
Wed, 17 Jul 2013 12:19:14 +0900 Christian Sternagel refactoring
Wed, 17 Jul 2013 17:16:51 +0200 wenzelm more robust exn_messages_ids;
Wed, 17 Jul 2013 14:33:33 +0200 wenzelm non-strict "Quiet" mode, to avoid odd crash of code_pred/after_qed due to ill-typed use of string_of_clause (e.g. in JinjaThreads/Common/Decl.thy of AFP/d1bb08f92ce5);
Wed, 17 Jul 2013 13:45:55 +0200 wenzelm take context from static theory, not dynamic theory certificate;
Wed, 17 Jul 2013 11:38:57 +0200 wenzelm more official Thm.eq_thm_strict, without demanding ML equality type;
Wed, 17 Jul 2013 09:32:08 +0200 wenzelm tuned;
Wed, 17 Jul 2013 13:34:21 +0200 immler tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
Tue, 16 Jul 2013 23:34:33 +0200 wenzelm merged
Tue, 16 Jul 2013 22:36:55 +0200 wenzelm Cygwin with Latex according to Cygwin-Latex-Setup.bat (presently unused);
Tue, 16 Jul 2013 20:23:05 +0200 wenzelm overwrite target;
Tue, 16 Jul 2013 18:28:45 +0200 wenzelm fully-automated packaging (requires Mac OS X);
Tue, 16 Jul 2013 14:46:03 +0200 wenzelm more robust application init;
Tue, 16 Jul 2013 14:10:10 +0200 wenzelm more self-contained application, with side-entry for init;
Tue, 16 Jul 2013 13:44:52 +0200 wenzelm dispose intermediate 7z archive;
Tue, 16 Jul 2013 13:27:01 +0200 wenzelm prefer stand-alone javaw;
Tue, 16 Jul 2013 13:23:37 +0200 wenzelm more robust executable path specifications;
Tue, 16 Jul 2013 12:31:08 +0200 wenzelm separate module XZ_File to avoid initial dependency on org.tukaani.xz;
Tue, 16 Jul 2013 12:25:59 +0200 wenzelm build Windows application on the spot, using Unix tools;
Mon, 15 Jul 2013 23:53:04 +0200 wenzelm recover Cygwin symlinks via Windows file-system operations;
Mon, 15 Jul 2013 23:07:23 +0200 wenzelm produce 7z archive for windows and preserve symlinks separately;
Mon, 15 Jul 2013 22:11:36 +0200 wenzelm Scala version of init.bat;
Mon, 15 Jul 2013 20:36:27 +0200 wenzelm tuned line length;
Mon, 15 Jul 2013 20:13:30 +0200 wenzelm prefer @{file} references that are actually checked;
Mon, 15 Jul 2013 19:51:09 +0200 wenzelm deactivate/revoke mouse event more thoroughly, to avoid "Implicit change of text area buffer";
Mon, 15 Jul 2013 19:23:19 +0200 wenzelm retain compile-time context visibility, which is particularly important for "apply tactic";
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip