Thu, 30 Jun 2011 19:24:09 +0200 wenzelm more general theory header parsing;
Thu, 30 Jun 2011 16:50:26 +0200 wenzelm back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
Thu, 30 Jun 2011 16:07:30 +0200 wenzelm merged
Thu, 30 Jun 2011 10:15:46 +0200 krauss parse term in auxiliary context augmented with variable;
Wed, 29 Jun 2011 11:58:35 +0200 boehmes linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
Thu, 30 Jun 2011 14:55:01 +0200 wenzelm prefer Isabelle path algebra;
Thu, 30 Jun 2011 14:51:32 +0200 wenzelm proper fold order;
Thu, 30 Jun 2011 14:03:31 +0200 wenzelm more Path operations;
Thu, 30 Jun 2011 13:59:55 +0200 wenzelm getenv_strict in ML;
Thu, 30 Jun 2011 13:21:41 +0200 wenzelm standardized use of Path operations;
Thu, 30 Jun 2011 11:15:36 +0200 wenzelm tuned comments;
Thu, 30 Jun 2011 00:09:57 +0200 wenzelm abstract algebra of file paths in Scala (cf. path.ML);
Thu, 30 Jun 2011 00:01:00 +0200 wenzelm proper Path.print;
Wed, 29 Jun 2011 23:43:48 +0200 wenzelm basic operations on lists and strings;
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Wed, 29 Jun 2011 18:12:34 +0200 wenzelm modernized some simproc setup;
Wed, 29 Jun 2011 17:35:46 +0200 wenzelm modernized some simproc setup;
Wed, 29 Jun 2011 16:31:50 +0200 wenzelm print Path.T with some markup;
Wed, 29 Jun 2011 15:23:36 +0200 wenzelm HTML: render control symbols more like Isabelle/Scala/jEdit;
Tue, 28 Jun 2011 10:52:15 +0200 traytel collapse map functions with identity subcoercions to identities;
Tue, 28 Jun 2011 21:06:59 +0200 blanchet reenabled accidentally-disabled automatic minimization
Tue, 28 Jun 2011 20:42:29 +0200 wenzelm tuned markup;
Tue, 28 Jun 2011 17:13:32 +0100 paulson merged
Tue, 28 Jun 2011 17:12:50 +0100 paulson tidied messy proofs
Tue, 28 Jun 2011 16:43:44 +0200 bulwahn merged
Tue, 28 Jun 2011 14:36:43 +0200 bulwahn adding timeout to quickcheck narrowing
Tue, 28 Jun 2011 14:52:46 +0100 paulson simplified proofs using metis calls
Tue, 28 Jun 2011 12:48:00 +0100 paulson merged
Tue, 28 Jun 2011 12:47:32 +0100 paulson keyfree: The set of key-free messages (and associated theorems)
Mon, 27 Jun 2011 22:44:44 +0200 wenzelm merged
Mon, 27 Jun 2011 17:04:04 +0200 krauss new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
Mon, 27 Jun 2011 14:56:39 +0200 blanchet added reference for MESON
Mon, 27 Jun 2011 14:56:37 +0200 blanchet document "meson" and "metis" in HOL specific section of the Isar ref manual
Mon, 27 Jun 2011 14:56:35 +0200 blanchet clarify minimizer output
Mon, 27 Jun 2011 14:56:33 +0200 blanchet don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
Mon, 27 Jun 2011 14:56:32 +0200 blanchet tweaked comment
Mon, 27 Jun 2011 14:56:31 +0200 blanchet document "sound" option
Mon, 27 Jun 2011 14:56:29 +0200 blanchet minor Sledgehammer news
Mon, 27 Jun 2011 14:56:28 +0200 blanchet added "sound" option to force Sledgehammer to be pedantically sound
Mon, 27 Jun 2011 14:56:26 +0200 blanchet removed "full_types" option from documentation
Mon, 27 Jun 2011 14:56:10 +0200 blanchet document changes to Sledgehammer and "try"
Mon, 27 Jun 2011 13:52:47 +0200 blanchet removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
Mon, 27 Jun 2011 13:52:47 +0200 blanchet clarify warning message to avoid confusing beginners
Mon, 27 Jun 2011 13:52:47 +0200 blanchet remove experimental trimming feature -- it slowed down things on Linux for some reason
Mon, 27 Jun 2011 13:52:47 +0200 blanchet filter out some tautologies using an ATP, especially for those theories that are known for producing such things
Mon, 27 Jun 2011 22:23:44 +0200 wenzelm NEWS;
Mon, 27 Jun 2011 22:20:49 +0200 wenzelm document antiquotations are managed as theory data, with proper name space and entity markup;
Mon, 27 Jun 2011 17:51:28 +0200 wenzelm proper checking of @{ML_antiquotation};
Mon, 27 Jun 2011 17:20:24 +0200 wenzelm hide rather short auxiliary names, which can easily occur in user theories;
Mon, 27 Jun 2011 17:06:06 +0200 wenzelm updated generated file;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Mon, 27 Jun 2011 15:03:55 +0200 wenzelm old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
Mon, 27 Jun 2011 15:01:08 +0200 wenzelm parallel Syntax.parse, which is rather slow;
Mon, 27 Jun 2011 14:38:58 +0200 wenzelm markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
Mon, 27 Jun 2011 09:42:46 +0200 hoelzl move conditional expectation to its own theory file
Sun, 26 Jun 2011 19:10:03 +0200 boehmes updated SMT certificates
Sun, 26 Jun 2011 19:10:02 +0200 boehmes generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
Sat, 25 Jun 2011 20:03:07 +0200 wenzelm proper tokens only if session is ready;
Sat, 25 Jun 2011 19:38:35 +0200 wenzelm entity markup for "type", "constant";
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip