2010-08-26 wenzelm misc tuning and simplification, notably theory data;
2010-08-26 wenzelm 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 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 standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
2010-08-26 wenzelm merged
2010-08-26 blanchet merged
2010-08-26 blanchet consider "locality" when assigning weights to facts
2010-08-26 blanchet add a bonus for chained facts, since they are likely to be relevant;
2010-08-26 blanchet merged
2010-08-25 blanchet add a penalty for lambda-abstractions;
2010-08-25 blanchet renaming
2010-08-25 blanchet fiddle with relevance filter
2010-08-25 blanchet update docs
2010-08-25 blanchet reorganize options regarding to the relevance threshold and decay
2010-08-25 blanchet make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
2010-08-25 blanchet simplify more code
2010-08-25 blanchet cosmetics
2010-08-25 blanchet get rid of "defs_relevant" feature;
2010-08-25 blanchet make SML/NJ happy
2010-08-25 blanchet renamed "relevance_convergence" to "relevance_decay"
2010-08-24 blanchet 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 better workaround for E's off-by-one-second issue
2010-08-26 bulwahn merged
2010-08-25 bulwahn renaming variables to conform to prolog names
2010-08-25 bulwahn changing hotel trace definition; adding simple handling of numerals on natural numbers
2010-08-25 bulwahn added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
2010-08-25 bulwahn moving preprocessing to values in prolog generation
2010-08-25 bulwahn invocation of values for prolog execution does not require invocation of code_pred anymore
2010-08-25 bulwahn adding hotel keycard example for prolog generation
2010-08-25 bulwahn improving output of set comprehensions; adding style_check flags
2010-08-25 bulwahn improving ensure_groundness in prolog generation; added further example
2010-08-25 bulwahn adding very basic transformation to ensure groundness before negations
2010-08-26 wenzelm Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
2010-08-26 wenzelm tuned signature;
2010-08-25 wenzelm Pretty: tuned markup objects;
2010-08-25 wenzelm tuned;
2010-08-25 wenzelm organized markup properties via apply/unapply patterns;
2010-08-25 wenzelm added some proof state markup, notably number of subgoals (e.g. for indentation);
2010-08-25 wenzelm ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
2010-08-25 wenzelm merged
2010-08-25 Christian Urban tuned code
2010-08-25 Christian Urban quotient package: deal correctly with frees in lifted theorems
2010-08-25 wenzelm approximation_oracle: actually match true/false in ML, not arbitrary values;
2010-08-25 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-25 wenzelm more precise Command.State accumulation;
2010-08-25 wenzelm eliminated some old camel case stuff;
2010-08-25 wenzelm some attempts to recover Isabelle/ML style from the depths of time;
2010-08-25 wenzelm keep persistent production tables as immutable vectors -- potential performance improvement on modern hardware;
2010-08-25 wenzelm select tangible text ranges here -- more robust against ongoing changes of the markup query model
2010-08-25 wenzelm structure Thm: less pervasive names;
2010-08-25 wenzelm discontinued obsolete 'global' and 'local' commands;
2010-08-25 wenzelm merged
2010-08-25 hoelzl merged
2010-08-24 hoelzl moved generic lemmas in Probability to HOL
2010-08-25 wenzelm merged
2010-08-25 haftmann traling newline on standard output
2010-08-25 Cezary Kaliszyk Quotient Package / lemma for regularization of bex1_rel for equivalence relations
2010-08-24 blanchet merged
2010-08-24 blanchet make Mirabelle happy
2010-08-24 blanchet compute names lazily;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip