Mon, 07 Nov 2011 17:54:38 +0100 boehmes try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
Mon, 07 Nov 2011 17:54:35 +0100 boehmes replace higher-order matching against schematic theorem with dedicated reconstruction method
Mon, 07 Nov 2011 17:24:57 +0100 wenzelm merged
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
Mon, 07 Nov 2011 16:41:16 +0100 wenzelm discontinued numbered structure indexes (legacy feature);
Mon, 07 Nov 2011 16:39:14 +0100 wenzelm tuned proofs;
Mon, 07 Nov 2011 14:16:01 +0100 blanchet return outcome code, so that it can be picked up by Mutabelle
Mon, 07 Nov 2011 14:16:01 +0100 blanchet align columns in output and keep error log around
Mon, 07 Nov 2011 14:59:58 +0100 wenzelm offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
Mon, 07 Nov 2011 14:23:50 +0100 wenzelm clarified attribute "mono_set": pure declaration, proper export in ML;
Mon, 07 Nov 2011 14:14:20 +0100 wenzelm misc tuning;
Mon, 07 Nov 2011 12:08:22 +0100 wenzelm made SML/NJ happy;
Sun, 06 Nov 2011 22:18:54 +0100 blanchet more millisecond cleanup
Sun, 06 Nov 2011 22:18:54 +0100 blanchet updated documentation
Sun, 06 Nov 2011 22:18:54 +0100 blanchet try "smt" as a fallback for ATPs if "metis" fails/times out
Sun, 06 Nov 2011 22:18:54 +0100 blanchet more detailed preplay output
Sun, 06 Nov 2011 22:18:54 +0100 blanchet tuning
Sun, 06 Nov 2011 22:18:54 +0100 blanchet tuning
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Sun, 06 Nov 2011 21:17:45 +0100 wenzelm tuned;
Sun, 06 Nov 2011 18:42:17 +0100 wenzelm merged
Sun, 06 Nov 2011 14:23:04 +0100 blanchet cascading timeouts in minimizer, part 2
Sun, 06 Nov 2011 14:05:57 +0100 blanchet tuning
Sun, 06 Nov 2011 13:57:17 +0100 blanchet use "Time.time" rather than milliseconds internally
Sun, 06 Nov 2011 13:46:26 +0100 blanchet tune: no need for option
Sun, 06 Nov 2011 13:37:49 +0100 blanchet cascading timeouts in minimizer
Sun, 06 Nov 2011 13:32:13 +0100 blanchet shortcut binary minimization algorithm
Sun, 06 Nov 2011 11:51:35 +0100 blanchet speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half
Sun, 06 Nov 2011 11:16:37 +0100 blanchet renamed experimental systems
Sun, 06 Nov 2011 11:13:47 +0100 blanchet repaired quantification over type variables for non-TFF1/THF encodings
Sun, 06 Nov 2011 18:42:15 +0100 wenzelm misc tuning and modernization;
Sun, 06 Nov 2011 17:53:32 +0100 wenzelm misc tuning and modernization;
Sun, 06 Nov 2011 17:05:45 +0100 wenzelm tuned;
Sun, 06 Nov 2011 17:00:05 +0100 wenzelm some statespace benchmarks;
Sun, 06 Nov 2011 16:41:53 +0100 wenzelm write changed .prv files only, to avoid writing into src file-space by default;
Sun, 06 Nov 2011 16:29:22 +0100 wenzelm tuned document;
Sun, 06 Nov 2011 16:22:26 +0100 wenzelm more precise dependencies;
Sun, 06 Nov 2011 14:20:41 +0100 wenzelm inlined antiquotations;
Sun, 06 Nov 2011 14:09:24 +0100 wenzelm misc tuning and modernization;
Sun, 06 Nov 2011 13:25:41 +0100 wenzelm optional timing, to avoid redundant allocation of mutable cells;
Sat, 05 Nov 2011 22:41:25 +0100 wenzelm tuned;
Sat, 05 Nov 2011 22:01:19 +0100 wenzelm misc tuning;
Sat, 05 Nov 2011 21:36:56 +0100 wenzelm merged
Sat, 05 Nov 2011 12:01:21 +0000 Christian Urban more use of global operations (see 98ec8b51af9c)
Sat, 05 Nov 2011 20:40:30 +0100 wenzelm more uniform instT_subst vs. inst_subst: compare variable names only;
Sat, 05 Nov 2011 20:32:12 +0100 wenzelm tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
Sat, 05 Nov 2011 20:07:38 +0100 wenzelm misc tuning and modernization;
Sat, 05 Nov 2011 19:47:22 +0100 wenzelm some performance tuning via Term_Subst/Same.operation;
Sat, 05 Nov 2011 18:58:40 +0100 wenzelm pruned signature;
Sat, 05 Nov 2011 15:00:49 +0100 wenzelm added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
Sat, 05 Nov 2011 10:59:11 +0100 wenzelm more conventional syntax const;
Fri, 04 Nov 2011 20:16:42 +0100 wenzelm proper syntactic category for abstraction syntax, to avoid low-level exception for malformed "\<integral> x y. f \<partial>M", for example;
Fri, 04 Nov 2011 17:34:51 +0100 wenzelm merged
Fri, 04 Nov 2011 17:19:33 +0100 wenzelm prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
Fri, 04 Nov 2011 15:05:59 +0000 blanchet document new experimental provers
Fri, 04 Nov 2011 15:05:58 +0000 blanchet added remote iProver(-Eq) for experimentation
Fri, 04 Nov 2011 13:52:19 +0100 wenzelm merged
Fri, 04 Nov 2011 08:19:24 +0100 huffman ex/Tree23.thy: automate proof of gfull_add
Fri, 04 Nov 2011 08:00:48 +0100 huffman ex/Tree23.thy: simplify proof of bal_del0
Fri, 04 Nov 2011 07:37:37 +0100 huffman ex/Tree23.thy: simplify proof of bal_add0
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip