2010-08-25 haftmann 2010-08-25 tuned
2010-08-27 wenzelm 2010-08-27 proper context for various Thy_Output options, via official configuration options in ML and Isar;
2010-08-27 wenzelm 2010-08-27 Thy_Output: options based on proper context, although Thy_Output.add_wrapper still allows to maintain old-style wrapper combinators (setmp_CRITICAL etc.);
2010-08-27 wenzelm 2010-08-27 eliminated old 'local' command;
2010-08-26 wenzelm 2010-08-26 more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
2010-08-26 wenzelm 2010-08-26 Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
2010-08-26 wenzelm 2010-08-26 slightly more abstract data handling in Fast_Lin_Arith;
2010-08-26 wenzelm 2010-08-26 theory data merge: prefer left side uniformly;
2010-08-26 wenzelm 2010-08-26 tuned;
2010-08-26 wenzelm 2010-08-26 simplification/standardization of some theory data;
2010-08-26 wenzelm 2010-08-26 misc tuning and simplification, notably theory data;
2010-08-26 wenzelm 2010-08-26 renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-26 wenzelm 2010-08-26 renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-26 wenzelm 2010-08-26 standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
2010-08-26 wenzelm 2010-08-26 merged
2010-08-26 blanchet 2010-08-26 merged
2010-08-26 blanchet 2010-08-26 consider "locality" when assigning weights to facts
2010-08-26 blanchet 2010-08-26 add a bonus for chained facts, since they are likely to be relevant; (especially in a Mirabelle run!) -- chained facts used to be included forcibly, then were treated as any other fact; the current approach seems more flexible
2010-08-26 blanchet 2010-08-26 merged
2010-08-26 blanchet 2010-08-26 add a penalty for lambda-abstractions; the penalty will kick in only when the goal contains no lambdas, in which case Sledgehammer previously totally disallowed any higher-order construct; this was too drastic; lambdas are dangerous because they rapidly lead to unsound proofs; e.g. COMBI_def COMBS_def not_Cons_self2 with explicit_apply
2010-08-26 blanchet 2010-08-26 renaming
2010-08-26 blanchet 2010-08-26 fiddle with relevance filter
2010-08-25 blanchet 2010-08-25 update docs
2010-08-25 blanchet 2010-08-25 reorganize options regarding to the relevance threshold and decay
2010-08-25 blanchet 2010-08-25 make relevance filter work in term of a "max_relevant" option + use Vampire SOS; "max_relevant" is more reliable than "max_relevant_per_iter"; also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before; SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)
2010-08-25 blanchet 2010-08-25 simplify more code
2010-08-25 blanchet 2010-08-25 cosmetics
2010-08-25 blanchet 2010-08-25 get rid of "defs_relevant" feature; nobody uses it and it works poorly
2010-08-25 blanchet 2010-08-25 make SML/NJ happy
2010-08-25 blanchet 2010-08-25 renamed "relevance_convergence" to "relevance_decay"
2010-08-24 blanchet 2010-08-24 make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
2010-08-24 blanchet 2010-08-24 better workaround for E's off-by-one-second issue
2010-08-26 bulwahn 2010-08-26 merged
2010-08-25 bulwahn 2010-08-25 renaming variables to conform to prolog names
2010-08-25 bulwahn 2010-08-25 changing hotel trace definition; adding simple handling of numerals on natural numbers
2010-08-25 bulwahn 2010-08-25 added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
2010-08-25 bulwahn 2010-08-25 moving preprocessing to values in prolog generation
2010-08-25 bulwahn 2010-08-25 invocation of values for prolog execution does not require invocation of code_pred anymore
2010-08-25 bulwahn 2010-08-25 adding hotel keycard example for prolog generation
2010-08-25 bulwahn 2010-08-25 improving output of set comprehensions; adding style_check flags
2010-08-25 bulwahn 2010-08-25 improving ensure_groundness in prolog generation; added further example
2010-08-25 bulwahn 2010-08-25 adding very basic transformation to ensure groundness before negations
2010-08-26 wenzelm 2010-08-26 Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
2010-08-26 wenzelm 2010-08-26 tuned signature;
2010-08-25 wenzelm 2010-08-25 Pretty: tuned markup objects;
2010-08-25 wenzelm 2010-08-25 tuned;
2010-08-25 wenzelm 2010-08-25 organized markup properties via apply/unapply patterns;
2010-08-25 wenzelm 2010-08-25 added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;
2010-08-25 wenzelm 2010-08-25 ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
2010-08-25 wenzelm 2010-08-25 merged
2010-08-25 Christian Urban 2010-08-25 tuned code
2010-08-25 Christian Urban 2010-08-25 quotient package: deal correctly with frees in lifted theorems
2010-08-25 wenzelm 2010-08-25 approximation_oracle: actually match true/false in ML, not arbitrary values;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-25 wenzelm 2010-08-25 more precise Command.State accumulation;
2010-08-25 wenzelm 2010-08-25 eliminated some old camel case stuff;
2010-08-25 wenzelm 2010-08-25 some attempts to recover Isabelle/ML style from the depths of time;
2010-08-25 wenzelm 2010-08-25 keep persistent production tables as immutable vectors -- potential performance improvement on modern hardware;
2010-08-25 wenzelm 2010-08-25 select tangible text ranges here -- more robust against ongoing changes of the markup query model
2010-08-25 wenzelm 2010-08-25 structure Thm: less pervasive names;