Tue, 10 Sep 2013 15:56:51 +0200 blanchet got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)
Tue, 10 Sep 2013 15:56:51 +0200 blanchet avoid double traversal of term
Tue, 10 Sep 2013 15:56:51 +0200 blanchet got rid of old, needless logic
Tue, 10 Sep 2013 15:56:51 +0200 blanchet moved ML function closer to its remaining use
Tue, 10 Sep 2013 15:56:51 +0200 blanchet faster uniquification
Tue, 10 Sep 2013 15:56:51 +0200 blanchet stronger fact normalization
Tue, 10 Sep 2013 15:56:51 +0200 blanchet gracefully handle huge thys
Tue, 10 Sep 2013 15:56:51 +0200 blanchet speed up detection of simp rules
Tue, 10 Sep 2013 15:56:51 +0200 blanchet don't be so verbose about SMT solver failures
Tue, 10 Sep 2013 14:02:49 +0200 wenzelm tuned;
Tue, 10 Sep 2013 11:57:53 +0200 wenzelm more portable hash-bang;
Tue, 10 Sep 2013 11:46:51 +0200 wenzelm tuned signature;
Tue, 10 Sep 2013 00:22:12 +0200 wenzelm merged
Tue, 10 Sep 2013 00:18:30 +0200 wenzelm tuned proofs;
Mon, 09 Sep 2013 23:11:02 +0200 wenzelm tuned proofs;
Mon, 09 Sep 2013 23:55:35 +0200 blanchet make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices
Mon, 09 Sep 2013 23:54:59 +0200 blanchet since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion
Mon, 09 Sep 2013 23:09:37 +0200 blanchet more docs
Mon, 09 Sep 2013 20:24:15 +0200 wenzelm merged
Mon, 09 Sep 2013 17:28:08 +0200 wenzelm proper apple.awt.application.name for Java 7;
Mon, 09 Sep 2013 17:02:06 +0200 wenzelm generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
Mon, 09 Sep 2013 16:15:48 +0200 wenzelm more robust Mac OS X application support;
Mon, 09 Sep 2013 15:53:02 +0200 wenzelm use polyml-5.5.1 (SVN), to increase chances of stability of this test;
Mon, 09 Sep 2013 14:48:16 +0200 wenzelm override potential changes in $ISABELLE_HOME_USER/etc/settings;
Mon, 09 Sep 2013 14:22:39 +0200 wenzelm generate application ini based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);
Mon, 09 Sep 2013 13:48:06 +0200 wenzelm generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
Mon, 09 Sep 2013 18:14:54 +0200 blanchet tuning
Mon, 09 Sep 2013 18:12:41 +0200 blanchet made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents
Mon, 09 Sep 2013 15:22:04 +0200 blanchet limit the number of instances of a single theorem
Mon, 09 Sep 2013 15:22:04 +0200 blanchet move metis to new monomorphizer
Mon, 09 Sep 2013 15:22:04 +0200 blanchet use new monomorphizer in Sledgehammer
Mon, 09 Sep 2013 14:23:04 +0200 blanchet tuning
Mon, 09 Sep 2013 14:22:11 +0200 blanchet include map theorems in datastructure for "primcorec"
Mon, 09 Sep 2013 13:47:58 +0200 blanchet enriched data structure with necessary theorems
Sun, 08 Sep 2013 19:25:06 +0200 wenzelm updated exe -- more explicit icon;
Sun, 08 Sep 2013 18:37:42 +0200 wenzelm more official lib/logo/isabelle.bmp;
Sun, 08 Sep 2013 18:10:12 +0200 wenzelm use windows_app based on WinRun4J;
Sun, 08 Sep 2013 17:51:56 +0200 wenzelm updated to WinRun4J;
Sun, 08 Sep 2013 12:26:07 +0200 traytel tuned whitespace
Sun, 08 Sep 2013 12:26:05 +0200 traytel don't register "sequential" as a keyword for now as this breaks the parser for function
Sat, 07 Sep 2013 23:09:26 +0200 wenzelm tuned proofs;
Sat, 07 Sep 2013 20:12:38 +0200 wenzelm merged
Sat, 07 Sep 2013 19:45:36 +0200 wenzelm tuned message;
Sat, 07 Sep 2013 19:18:05 +0200 wenzelm tuned message;
Sat, 07 Sep 2013 18:37:25 +0200 wenzelm imitate "isabelle java" and "isabelle jedit" wrt. classpath and options (see also a221a4fdb5a0);
Sat, 07 Sep 2013 18:24:24 +0200 wenzelm generate application wrapper for Linux;
Sat, 07 Sep 2013 17:43:13 +0200 wenzelm observe "stopped" after Cygwin init (which is itself uninterruptible);
Sat, 07 Sep 2013 17:32:55 +0200 wenzelm clarified modules;
Sat, 07 Sep 2013 17:23:05 +0200 wenzelm tuned signature;
Sat, 07 Sep 2013 17:11:44 +0200 wenzelm Cygwin_Init based on System_Dialog;
Sat, 07 Sep 2013 16:33:10 +0200 wenzelm tuned imports;
Sat, 07 Sep 2013 15:28:16 +0200 wenzelm more robust exit;
Sat, 07 Sep 2013 15:10:33 +0200 wenzelm Build_Dialog based on System_Dialog;
Sat, 07 Sep 2013 14:14:25 +0200 wenzelm clarified close operations;
Sat, 07 Sep 2013 14:07:12 +0200 wenzelm clarified result;
Sat, 07 Sep 2013 13:59:47 +0200 wenzelm dialog for system processes, with optional output window;
Sat, 07 Sep 2013 11:36:03 +0200 wenzelm more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;
Sat, 07 Sep 2013 11:28:30 +0200 wenzelm odd workaround for scalac to enable nohup;
Sat, 07 Sep 2013 11:02:27 +0200 wenzelm odd workaround for scalac to enable nohup;
Sat, 07 Sep 2013 00:02:19 +0200 wenzelm build session before start of jedit;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip