Mon, 06 Dec 2010 13:33:09 +0100 blanchet tune indentation
Mon, 06 Dec 2010 13:33:09 +0100 blanchet removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
Mon, 06 Dec 2010 13:33:05 +0100 blanchet implemented All rules from new monotonicity calculus
Mon, 06 Dec 2010 13:30:57 +0100 blanchet fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints
Mon, 06 Dec 2010 13:30:38 +0100 blanchet started implementing the new monotonicity rules for application
Mon, 06 Dec 2010 13:30:36 +0100 blanchet implemented connectives in new monotonicity calculus
Mon, 06 Dec 2010 13:29:23 +0100 blanchet added "Neq" operator to monotonicity inference module
Mon, 06 Dec 2010 13:26:27 +0100 blanchet started implementing connectives in new monotonicity calculus
Mon, 06 Dec 2010 13:26:23 +0100 blanchet more work on frames in the new monotonicity calculus
Mon, 06 Dec 2010 13:18:25 +0100 blanchet support 3 monotonicity calculi in one and fix soundness bug
Mon, 06 Dec 2010 13:18:25 +0100 blanchet tuning
Mon, 06 Dec 2010 13:18:25 +0100 blanchet proper handling of assignment disjunctions vs. conjunctions
Mon, 06 Dec 2010 13:18:25 +0100 blanchet adapt monotonicity code to four annotation types
Mon, 06 Dec 2010 13:18:25 +0100 blanchet more monotonicity tuning
Mon, 06 Dec 2010 13:18:25 +0100 blanchet tuning
Mon, 06 Dec 2010 13:18:25 +0100 blanchet added frame component to Gamma in monotonicity calculus
Mon, 06 Dec 2010 13:18:25 +0100 blanchet use boolean pair to encode annotation, which may now take four values
Mon, 06 Dec 2010 13:18:25 +0100 blanchet started generalizing monotonicity code to accommodate new calculus
Mon, 06 Dec 2010 13:17:26 +0100 blanchet merged
Mon, 06 Dec 2010 11:41:24 +0100 blanchet handle "max_relevant" uniformly
Mon, 06 Dec 2010 11:26:17 +0100 blanchet honor the default max relevant facts setting from the SMT solvers in Sledgehammer
Mon, 06 Dec 2010 11:25:21 +0100 blanchet have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
Mon, 06 Dec 2010 10:32:39 +0100 blanchet return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
Mon, 06 Dec 2010 10:31:29 +0100 blanchet trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
Mon, 06 Dec 2010 10:23:31 +0100 blanchet reraise interrupt exceptions
Mon, 06 Dec 2010 09:54:58 +0100 blanchet [mq]: sledge_binary_minimizer
Mon, 06 Dec 2010 10:52:48 +0100 bulwahn correcting usage documentation in mirabelle tool
Mon, 06 Dec 2010 10:52:46 +0100 bulwahn adding mutabelle as a component and an isabelle tool to be used in regression testing
Mon, 06 Dec 2010 10:52:45 +0100 bulwahn commenting out sledgehammer_mtd in Mutabelle
Mon, 06 Dec 2010 10:52:45 +0100 bulwahn removing declaration in quickcheck to really enable exhaustive testing
Mon, 06 Dec 2010 10:52:44 +0100 bulwahn adding timeout to try invocation in mutabelle
Mon, 06 Dec 2010 10:52:43 +0100 bulwahn adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
Mon, 06 Dec 2010 09:34:57 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Mon, 06 Dec 2010 09:25:05 +0100 haftmann moved bootstrap of type_lifting to Fun
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Mon, 06 Dec 2010 14:45:29 +0100 wenzelm avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
Sun, 05 Dec 2010 15:23:33 +0100 wenzelm IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
Sun, 05 Dec 2010 14:02:16 +0100 wenzelm command 'notepad' replaces former 'example_proof';
Sun, 05 Dec 2010 13:42:58 +0100 wenzelm prefer 'notepad' over 'example_proof';
Sun, 05 Dec 2010 08:34:02 +0100 haftmann merged
Sat, 04 Dec 2010 21:53:00 +0100 haftmann more intimate definition of fold_list / fold_once in terms of fold
Sat, 04 Dec 2010 21:26:33 +0100 haftmann canonical fold signature
Sat, 04 Dec 2010 21:26:55 +0100 wenzelm formal notepad without any result;
Sat, 04 Dec 2010 18:41:12 +0100 wenzelm added Syntax.default_root;
Sat, 04 Dec 2010 15:14:28 +0100 wenzelm eliminated obsolete Token.Malformed -- subsumed by Token.Error;
Sat, 04 Dec 2010 14:59:25 +0100 wenzelm tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);
Sat, 04 Dec 2010 14:57:04 +0100 wenzelm added Syntax.pretty_priority;
Fri, 03 Dec 2010 22:40:26 +0100 haftmann merged
Fri, 03 Dec 2010 14:46:58 +0100 haftmann conventional point-free characterization of rsp_fold
Fri, 03 Dec 2010 14:39:15 +0100 haftmann replaced memb by existing List.member
Fri, 03 Dec 2010 14:22:24 +0100 haftmann explicit type constraint;
Fri, 03 Dec 2010 22:39:34 +0100 haftmann tuned proposition
Fri, 03 Dec 2010 22:34:20 +0100 haftmann lemma multiset_of_rev
Fri, 03 Dec 2010 22:34:20 +0100 haftmann lemmas fold_remove1_split and fold_multiset_equiv
Fri, 03 Dec 2010 22:08:14 +0100 wenzelm minor tuning for release;
Fri, 03 Dec 2010 21:34:54 +0100 wenzelm source files are always encoded as UTF-8;
Fri, 03 Dec 2010 21:30:41 +0100 wenzelm eliminated fragile HTML.with_charset -- always use utf-8;
Fri, 03 Dec 2010 20:38:58 +0100 wenzelm recoded latin1 as utf8;
Fri, 03 Dec 2010 20:26:57 +0100 wenzelm removed old generated stuff;
Fri, 03 Dec 2010 20:02:57 +0100 wenzelm comment;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip