Wed, 10 Nov 2010 15:42:20 +0100 wenzelm proper treatment of equal heading level;
Wed, 10 Nov 2010 15:41:29 +0100 wenzelm added missing Keyword.THY_SCHEMATIC_GOAL;
Wed, 10 Nov 2010 15:17:25 +0100 wenzelm default Sidekick parser based on section headings;
Wed, 10 Nov 2010 15:00:40 +0100 wenzelm some support for nested source structure, based on section headings;
Wed, 10 Nov 2010 11:44:35 +0100 wenzelm tuned;
Tue, 09 Nov 2010 23:24:46 +0100 wenzelm misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
Tue, 09 Nov 2010 22:37:10 +0100 wenzelm updated version;
Tue, 09 Nov 2010 21:52:05 +0100 wenzelm private counter, to keep externalized ids a bit smaller;
Tue, 09 Nov 2010 21:44:19 +0100 wenzelm added general Synchronized.counter convenience;
Tue, 09 Nov 2010 21:13:06 +0100 wenzelm explicitly identify forked/joined tasks;
Tue, 09 Nov 2010 11:27:58 +0100 wenzelm accomodate old manuals that include pdfsetup.sty without isabelle.sty;
Tue, 09 Nov 2010 11:17:15 +0100 wenzelm merged
Mon, 08 Nov 2010 23:02:20 +0100 krauss removed type-inference-like behaviour from relation_tac completely; tuned
Mon, 08 Nov 2010 20:55:27 +0100 wenzelm avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
Mon, 08 Nov 2010 20:50:56 +0100 wenzelm explicitly check uniqueness of symbol recoding;
Mon, 08 Nov 2010 17:44:47 +0100 wenzelm more hints on building and running Isabelle/jEdit from command line;
Mon, 08 Nov 2010 14:41:11 +0100 wenzelm merged
Mon, 08 Nov 2010 14:33:54 +0100 blanchet merge
Mon, 08 Nov 2010 14:33:30 +0100 blanchet reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
Mon, 08 Nov 2010 05:07:18 -0800 huffman merged
Sat, 06 Nov 2010 10:01:00 -0700 huffman merged
Fri, 05 Nov 2010 15:15:28 -0700 huffman (infixl "<<" 55) -> (infix "<<" 50)
Wed, 03 Nov 2010 17:22:25 -0700 huffman simplify some proofs
Wed, 03 Nov 2010 17:06:21 -0700 huffman remove unnecessary stuff from Discrete.thy
Wed, 03 Nov 2010 16:39:23 -0700 huffman remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
Wed, 03 Nov 2010 15:57:39 -0700 huffman add lemma eq_imp_below
Wed, 03 Nov 2010 15:47:46 -0700 huffman discontinue a bunch of legacy theorem names
Wed, 03 Nov 2010 15:31:24 -0700 huffman move a few admissibility lemmas into FOCUS/Stream_adm.thy
Wed, 03 Nov 2010 15:03:16 -0700 huffman simplify some proofs
Mon, 08 Nov 2010 13:53:18 +0100 blanchet compile -- 7550b2cba1cb broke the build
Mon, 08 Nov 2010 13:25:00 +0100 blanchet merge
Mon, 08 Nov 2010 09:10:44 +0100 blanchet recognize Vampire error
Mon, 08 Nov 2010 12:13:51 +0100 boehmes return the process return code along with the process outputs
Mon, 08 Nov 2010 12:13:44 +0100 boehmes better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
Mon, 08 Nov 2010 11:49:28 +0100 haftmann merged
Mon, 08 Nov 2010 10:56:48 +0100 haftmann corrected slip: must keep constant map, not type map; tuned code
Mon, 08 Nov 2010 10:43:24 +0100 haftmann constructors to datatypes in code_reflect can be globbed; dropped unused code
Mon, 08 Nov 2010 09:25:43 +0100 bulwahn adding code and theory for smallvalue generators, but do not setup the interpretation yet
Mon, 08 Nov 2010 02:33:48 +0100 blanchet make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
Mon, 08 Nov 2010 02:32:27 +0100 blanchet better detection of completely irrelevant facts
Sun, 07 Nov 2010 18:19:04 +0100 blanchet always use a hard timeout in Mirabelle
Sun, 07 Nov 2010 18:15:13 +0100 blanchet use "smt" (rather than "metis") to reconstruct SMT proofs
Sun, 07 Nov 2010 18:03:24 +0100 blanchet don't pass too many facts on the first iteration of the SMT solver
Sun, 07 Nov 2010 18:02:02 +0100 blanchet catch TimeOut exception
Sun, 07 Nov 2010 17:56:07 +0100 blanchet ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
Sun, 07 Nov 2010 17:51:25 +0100 blanchet if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
Sun, 07 Nov 2010 13:29:59 +0100 blanchet removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
Sat, 06 Nov 2010 10:25:08 +0100 blanchet make Nitpick datatype tests faster to make timeout less likely
Sat, 06 Nov 2010 10:25:08 +0100 blanchet invoke SMT solver in a loop, with fewer and fewer facts, in case of error
Sat, 06 Nov 2010 10:25:08 +0100 blanchet always honor the max relevant constraint
Mon, 08 Nov 2010 11:28:22 +0100 wenzelm more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
Mon, 08 Nov 2010 00:00:47 +0100 wenzelm updated generated files;
Sun, 07 Nov 2010 23:32:26 +0100 wenzelm tweaked pdf setup to allow modification of \pdfminorversion;
Sun, 07 Nov 2010 23:12:40 +0100 wenzelm merged;
Sun, 07 Nov 2010 23:12:21 +0100 wenzelm updated generated files;
Sun, 07 Nov 2010 22:51:16 +0100 wenzelm basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
Sun, 07 Nov 2010 22:42:49 +0100 wenzelm updated generated file;
Sun, 07 Nov 2010 22:26:25 +0100 wenzelm more literal appearance of antiqopen/antiqclose;
Sun, 07 Nov 2010 16:39:03 +0100 wenzelm 'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
Sat, 06 Nov 2010 20:59:59 +0100 wenzelm continue after failed commands;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip