Mon, 09 Aug 2010 13:43:01 +0200 haftmann minimize sorts in certificate instantiation
Mon, 09 Aug 2010 14:08:30 +0200 blanchet prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
Mon, 09 Aug 2010 14:00:32 +0200 blanchet adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
Mon, 09 Aug 2010 13:46:25 +0200 blanchet "declare" -> "declaration" (typo)
Mon, 09 Aug 2010 12:53:16 +0200 blanchet replace "setup" with "declaration"
Mon, 09 Aug 2010 12:48:40 +0200 blanchet disable Nitpick on Cygwin while I'm on vacation;
Mon, 09 Aug 2010 12:42:25 +0200 blanchet merged
Mon, 09 Aug 2010 12:40:15 +0200 blanchet use "declaration" instead of "setup" to register Nitpick extensions
Mon, 09 Aug 2010 12:07:59 +0200 blanchet remove needless "open"
Mon, 09 Aug 2010 12:05:48 +0200 blanchet move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
Mon, 09 Aug 2010 11:05:45 +0200 blanchet fiddle some more with "max_new_relevant_facts_per_iter"
Mon, 09 Aug 2010 11:03:54 +0200 blanchet replace recursion with "fold"
Mon, 09 Aug 2010 10:39:53 +0200 blanchet remove debugging output
Mon, 09 Aug 2010 10:38:57 +0200 blanchet remove now needless "Thm.transfer"
Mon, 09 Aug 2010 10:13:18 +0200 blanchet reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF
Mon, 09 Aug 2010 09:57:50 +0200 blanchet merge
Mon, 09 Aug 2010 09:57:38 +0200 blanchet fix embarrassing bug in elim rule handling, introduced during the port to FOF
Fri, 06 Aug 2010 21:10:29 +0200 blanchet minor doc changes
Wed, 11 Aug 2010 12:40:08 +0200 wenzelm modernized some specifications;
Wed, 11 Aug 2010 00:47:09 +0200 wenzelm tuned;
Wed, 11 Aug 2010 00:46:07 +0200 wenzelm Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
Wed, 11 Aug 2010 00:44:48 +0200 wenzelm native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
Wed, 11 Aug 2010 00:42:40 +0200 wenzelm proper handling of empty text;
Wed, 11 Aug 2010 00:42:01 +0200 wenzelm more uniform XML/YXML string_of_body/string_of_tree;
Tue, 10 Aug 2010 23:03:48 +0200 wenzelm type XML.Body as basic data representation language (Scala version);
Tue, 10 Aug 2010 22:26:23 +0200 wenzelm type XML.body as basic data representation language;
Tue, 10 Aug 2010 20:13:52 +0200 wenzelm renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
Tue, 10 Aug 2010 18:24:16 +0200 wenzelm added string_bytes convenience;
Tue, 10 Aug 2010 18:23:12 +0200 wenzelm tuned;
Tue, 10 Aug 2010 15:12:45 +0200 wenzelm removed obsolete methods for (ML) commands;
Tue, 10 Aug 2010 14:24:13 +0200 wenzelm prefer Nimbus look and feel on all platforms, instead of the somewhat ugly javax.swing.plaf.metal.MetalLookAndFeel, which presumably is implicit fall-back nonetheless;
Tue, 10 Aug 2010 14:15:50 +0200 wenzelm edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
Tue, 10 Aug 2010 12:29:11 +0200 wenzelm distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
Tue, 10 Aug 2010 12:09:53 +0200 wenzelm added Library.thread_actor -- thread as actor;
Tue, 10 Aug 2010 12:08:24 +0200 wenzelm clarified JEDIT_JAVA_OPTIONS vs. JEDIT_SYSTEM_OPTIONS -- discontinued JEDIT_APPLE_PROPERTIES;
Mon, 09 Aug 2010 22:02:26 +0200 wenzelm auto_flush: higher frequency;
Mon, 09 Aug 2010 21:35:45 +0200 wenzelm uniform raw_dump for input/output fifos on Cygwin;
Mon, 09 Aug 2010 21:23:24 +0200 wenzelm more robust fifo rendezvous: Cygwin 1.7 does not really block as expected;
Mon, 09 Aug 2010 18:18:32 +0200 wenzelm Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
Mon, 09 Aug 2010 13:56:02 +0200 wenzelm tuned comments;
Mon, 09 Aug 2010 11:45:30 +0200 wenzelm merged
Mon, 09 Aug 2010 11:38:32 +0200 haftmann added Lars Noschinski to isatest report
Mon, 09 Aug 2010 11:21:05 +0200 wenzelm merged
Sun, 08 Aug 2010 20:51:02 +0200 haftmann discontinued separation of `define` and `declare_const`
Sun, 08 Aug 2010 20:41:25 +0200 haftmann unravelled target initialization code
Sun, 08 Aug 2010 08:39:45 +0200 boehmes added filter for Boogie verification conditions (to prune assertions already proved by Boogie/Z3)
Sun, 08 Aug 2010 04:28:51 +0200 boehmes added scanning of if-then-else expressions
Fri, 06 Aug 2010 18:14:18 +0200 blanchet merged
Fri, 06 Aug 2010 18:11:30 +0200 blanchet added support for partial quotient types;
Fri, 06 Aug 2010 17:23:11 +0200 blanchet adapt occurrences of renamed Nitpick functions
Fri, 06 Aug 2010 17:18:29 +0200 blanchet document the non-legacy interfaces
Fri, 06 Aug 2010 17:05:29 +0200 blanchet local versions of Nitpick.register_xxx functions
Sun, 08 Aug 2010 22:33:41 +0200 wenzelm parse_spans: somewhat faster low-level implementation;
Sun, 08 Aug 2010 20:03:31 +0200 wenzelm proper context for Syntax.parse_token;
Sun, 08 Aug 2010 19:54:54 +0200 wenzelm prefer Context_Position.report where a proper context is available -- notably for "inner" entities;
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
Sun, 08 Aug 2010 14:22:54 +0200 wenzelm fixed odd runtime type error, which appears to have escaped the scala-2.8.0.final compiler;
Sun, 08 Aug 2010 14:00:59 +0200 wenzelm YXML.parse: refrain from interning, let XML.Cache do it (partially);
Sun, 08 Aug 2010 13:59:57 +0200 wenzelm cache_string: store trimmed string value;
Sat, 07 Aug 2010 23:02:19 +0200 wenzelm simple_dialog: allow scala.swing.Component as well;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip