Mon, 20 Sep 2010 09:19:17 +0200 haftmann updated file duplicate
Mon, 20 Sep 2010 09:19:13 +0200 haftmann \\isatypewrite now part of isabelle latex style
Mon, 20 Sep 2010 08:53:37 +0200 haftmann made smlnj happy
Sun, 19 Sep 2010 11:33:39 +0200 boehmes properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
Sun, 19 Sep 2010 00:29:13 +0200 boehmes do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
Fri, 17 Sep 2010 20:53:50 +0200 haftmann generalized lemma insort_remove1 to insort_key_remove1
Fri, 17 Sep 2010 20:53:50 +0200 haftmann generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
Fri, 17 Sep 2010 20:13:07 +0200 haftmann merged
Fri, 17 Sep 2010 17:17:56 +0200 haftmann less intermediate data structures
Mon, 20 Sep 2010 11:38:14 +0200 wenzelm Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
Sun, 19 Sep 2010 23:38:34 +0200 wenzelm simplified Isabelle_System.mk_fifo: inlined script, append PPID and PID uniformly;
Sun, 19 Sep 2010 22:40:22 +0200 wenzelm refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
Sun, 19 Sep 2010 22:20:48 +0200 wenzelm back to default fold painter -- Circle looks slightly odd in conjunction with bracket matching;
Sun, 19 Sep 2010 20:11:51 +0200 wenzelm message_actor: more robust treatment of EOF;
Sun, 19 Sep 2010 17:12:34 +0200 wenzelm simplified Isabelle_Process message kinds;
Sat, 18 Sep 2010 21:33:56 +0200 wenzelm recovered basic session stop/restart;
Sat, 18 Sep 2010 21:10:07 +0200 wenzelm simplified fifo handling -- rm_fifo always succeeds without ever blocking;
Sat, 18 Sep 2010 20:07:48 +0200 wenzelm raw_execute: let IOException pass-through unhindered (again);
Sat, 18 Sep 2010 19:38:27 +0200 wenzelm mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default;
Sat, 18 Sep 2010 17:39:23 +0200 wenzelm Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process);
Sat, 18 Sep 2010 17:14:47 +0200 wenzelm slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;
Sat, 18 Sep 2010 17:11:39 +0200 wenzelm tuned;
Sat, 18 Sep 2010 16:05:12 +0200 wenzelm separate Isabelle.logic_selector;
Sat, 18 Sep 2010 15:50:29 +0200 wenzelm non-editable text area;
Sat, 18 Sep 2010 14:28:42 +0200 wenzelm basic setup for prover session panel;
Fri, 17 Sep 2010 22:42:07 +0200 wenzelm ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
Fri, 17 Sep 2010 22:17:57 +0200 wenzelm discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
Fri, 17 Sep 2010 21:50:44 +0200 wenzelm Isabelle_Markup.overview_color: indicate error / warning messages;
Fri, 17 Sep 2010 21:49:34 +0200 wenzelm some specific message classification;
Fri, 17 Sep 2010 21:04:56 +0200 wenzelm Syntax.read_asts error: report token ranges within message -- no side-effect here;
Fri, 17 Sep 2010 20:56:32 +0200 wenzelm Isabelle_Process: status/report do not require serial numbers;
Fri, 17 Sep 2010 20:42:26 +0200 wenzelm simplified some internal flags using Config.T instead of full-blown Proof_Data;
Fri, 17 Sep 2010 20:18:27 +0200 wenzelm tuned signature of (Context_)Position.report variants;
Fri, 17 Sep 2010 17:31:20 +0200 wenzelm merged
Fri, 17 Sep 2010 16:38:11 +0200 blanchet merged
Fri, 17 Sep 2010 01:59:43 +0200 blanchet update README
Fri, 17 Sep 2010 01:59:30 +0200 blanchet regenerate "metis.ML"
Fri, 17 Sep 2010 01:58:21 +0200 blanchet fix license
Fri, 17 Sep 2010 01:56:19 +0200 blanchet updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
Fri, 17 Sep 2010 01:22:01 +0200 blanchet move functions around
Fri, 17 Sep 2010 00:54:56 +0200 blanchet simplify Skolem handling;
Fri, 17 Sep 2010 00:35:19 +0200 blanchet make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
Thu, 16 Sep 2010 17:30:29 +0200 blanchet complete refactoring of Metis along the lines of Sledgehammer
Thu, 16 Sep 2010 16:54:42 +0200 blanchet got caught once again by SML's pattern maching (ctor vs. var)
Thu, 16 Sep 2010 16:24:23 +0200 blanchet added new "Metis_Reconstruct" module, temporarily empty
Thu, 16 Sep 2010 16:12:02 +0200 blanchet rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
Thu, 16 Sep 2010 15:38:46 +0200 blanchet move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
Thu, 16 Sep 2010 15:28:16 +0200 blanchet skip some "important" messages
Thu, 16 Sep 2010 15:16:08 +0200 blanchet refactoring: move ATP proof and error extraction code to "ATP_Proof" module
Fri, 17 Sep 2010 16:15:45 +0200 nipkow merged
Fri, 17 Sep 2010 16:15:33 +0200 nipkow added lemmas
Fri, 17 Sep 2010 12:26:57 +0200 haftmann merged
Fri, 17 Sep 2010 11:05:53 +0200 haftmann proper closures for static evaluation; no need for FIXMEs any longer
Fri, 17 Sep 2010 11:05:51 +0200 haftmann refined static_eval_conv_simple; tuned comments
Fri, 17 Sep 2010 10:00:01 +0200 haftmann closures preserve static serializer context for static evaluation; tuned
Fri, 17 Sep 2010 09:21:49 +0200 haftmann closures separate serializer initialization from serializer invocation as far as appropriate
Fri, 17 Sep 2010 10:52:35 +0200 boehmes add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
Fri, 17 Sep 2010 08:41:07 +0200 haftmann made sml/nj happy
Thu, 16 Sep 2010 17:52:00 +0200 haftmann merged
Thu, 16 Sep 2010 17:31:51 +0200 haftmann added code_stmts antiquotation from doc-src/more_antiquote.ML
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip