wenzelm [Sat, 18 Sep 2010 16:05:12 +0200] rev 39517
separate Isabelle.logic_selector;
wenzelm [Sat, 18 Sep 2010 15:50:29 +0200] rev 39516
non-editable text area;
wenzelm [Sat, 18 Sep 2010 14:28:42 +0200] rev 39515
basic setup for prover session panel;
wenzelm [Fri, 17 Sep 2010 22:42:07 +0200] rev 39514
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
wenzelm [Fri, 17 Sep 2010 22:17:57 +0200] rev 39513
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);
wenzelm [Fri, 17 Sep 2010 21:50:44 +0200] rev 39512
Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm [Fri, 17 Sep 2010 21:49:34 +0200] rev 39511
some specific message classification;
wenzelm [Fri, 17 Sep 2010 21:04:56 +0200] rev 39510
Syntax.read_asts error: report token ranges within message -- no side-effect here;
wenzelm [Fri, 17 Sep 2010 20:56:32 +0200] rev 39509
Isabelle_Process: status/report do not require serial numbers;
wenzelm [Fri, 17 Sep 2010 20:42:26 +0200] rev 39508
simplified some internal flags using Config.T instead of full-blown Proof_Data;
wenzelm [Fri, 17 Sep 2010 20:18:27 +0200] rev 39507
tuned signature of (Context_)Position.report variants;
wenzelm [Fri, 17 Sep 2010 17:31:20 +0200] rev 39506
merged
blanchet [Fri, 17 Sep 2010 16:38:11 +0200] rev 39505
merged
blanchet [Fri, 17 Sep 2010 01:59:43 +0200] rev 39504
update README
blanchet [Fri, 17 Sep 2010 01:59:30 +0200] rev 39503
regenerate "metis.ML"
blanchet [Fri, 17 Sep 2010 01:58:21 +0200] rev 39502
fix license
blanchet [Fri, 17 Sep 2010 01:56:19 +0200] rev 39501
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet [Fri, 17 Sep 2010 01:22:01 +0200] rev 39500
move functions around
blanchet [Fri, 17 Sep 2010 00:54:56 +0200] rev 39499
simplify Skolem handling;
things are much easier now that Sledgehammer doesn't skolemize, only Metis
blanchet [Fri, 17 Sep 2010 00:35:19 +0200] rev 39498
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet [Thu, 16 Sep 2010 17:30:29 +0200] rev 39497
complete refactoring of Metis along the lines of Sledgehammer
blanchet [Thu, 16 Sep 2010 16:54:42 +0200] rev 39496
got caught once again by SML's pattern maching (ctor vs. var)
blanchet [Thu, 16 Sep 2010 16:24:23 +0200] rev 39495
added new "Metis_Reconstruct" module, temporarily empty
blanchet [Thu, 16 Sep 2010 16:12:02 +0200] rev 39494
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"