2011-05-12 blanchet 2011-05-12 use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
2011-05-12 blanchet 2011-05-12 further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
2011-05-12 blanchet 2011-05-12 reenabled equality proxy in Metis for higher-order reasoning
2011-05-12 blanchet 2011-05-12 added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file
2011-05-12 blanchet 2011-05-12 reflect option renaming in doc + do not document the type systems poly_preds? and poly_tags?, since they are virtually identical to the non-? versions
2011-05-12 blanchet 2011-05-12 unfold set constants in Sledgehammer/ATP as well if Metis does it too
2011-05-12 blanchet 2011-05-12 do not pollute relevance filter facts with too many facts about the boring set constants Collect and mem_def, which we might anyway unfold depending on Meson's settings
2011-05-12 blanchet 2011-05-12 renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12 blanchet 2011-05-12 added unfold set constant functionality to Meson/Metis -- disabled by default for now
2011-05-12 blanchet 2011-05-12 remove unused parameter
2011-05-12 blanchet 2011-05-12 reduced penalty associated with existential quantifiers
2011-05-12 blanchet 2011-05-12 ensure that Auto Sledgehammer is run with full type information
2011-05-12 blanchet 2011-05-12 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
2011-05-12 blanchet 2011-05-12 don't give weights to built-in symbols
2011-05-12 blanchet 2011-05-12 more robust exception handling in Metis (also works if there are several subgoals)
2011-05-12 blanchet 2011-05-12 no penality for constants that appear in chained facts
2011-05-12 blanchet 2011-05-12 gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers
2011-05-12 blanchet 2011-05-12 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
2011-05-12 blanchet 2011-05-12 tune whitespace
2011-05-12 blanchet 2011-05-12 added configuration options for experimental features
2011-05-12 blanchet 2011-05-12 ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
2011-05-12 blanchet 2011-05-12 avoid "Empty" exception by making sure that a certain optimization only is attempted when it makes sense
2011-05-12 blanchet 2011-05-12 added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
2011-05-12 blanchet 2011-05-12 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-12 blanchet 2011-05-12 allow each slice to have its own type system
2011-05-12 blanchet 2011-05-12 renamed type systems for more consistency
2011-05-12 wenzelm 2011-05-12 updated versions;
2011-05-12 wenzelm 2011-05-12 added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
2011-05-12 wenzelm 2011-05-12 tuned;
2011-05-12 wenzelm 2011-05-12 minor adaption for scala-2.9.0.final;
2011-05-12 wenzelm 2011-05-12 proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose;
2011-05-12 wenzelm 2011-05-12 pretend that all versions of BSD are Linux, which might actually work due to binary compatibilty mode of these obsolete platforms;
2011-05-12 haftmann 2011-05-12 more uniform naming of lemma
2011-05-09 noschinl 2011-05-09 add a lemma about commutative append to List.thy
2011-05-09 noschinl 2011-05-09 removed assumption from lemma List.take_add
2011-05-06 wenzelm 2011-05-06 no need for underscore.sty -- latex.ltx provides \textunderscore and \_ already;
2011-05-06 wenzelm 2011-05-06 removed \underscoreon which is from Larry's iman.sty, not underscore.sty;
2011-05-06 blanchet 2011-05-06 further improved type system setup based on Judgment Days
2011-05-06 blanchet 2011-05-06 allow each prover to specify its own formula kind for symbols occurring in the conjecture
2011-05-06 blanchet 2011-05-06 better type system setup, based on Judgment Day
2011-05-06 bulwahn 2011-05-06 improving merge of code specifications by removing code equations of constructors after merging two theories
2011-05-05 wenzelm 2011-05-05 tuned;
2011-05-05 wenzelm 2011-05-05 tuned some syntax names;
2011-05-05 wenzelm 2011-05-05 tuned rail diagrams and layout;
2011-05-05 wenzelm 2011-05-05 merged;
2011-05-05 blanchet 2011-05-05 tuning
2011-05-05 blanchet 2011-05-05 reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems
2011-05-05 blanchet 2011-05-05 added FIXME
2011-05-05 blanchet 2011-05-05 no lies in debug output (e.g. "slice 2 of 1")
2011-05-05 blanchet 2011-05-05 help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check
2011-05-05 blanchet 2011-05-05 query typedefs as well for monotonicity
2011-05-05 bulwahn 2011-05-05 adding examples for invoking quickcheck with records
2011-05-05 bulwahn 2011-05-05 adding creation of exhaustive generators for records; simplifying dependencies in Main theory
2011-05-05 blanchet 2011-05-05 hopefully this will help the SML/NJ type inference
2011-05-05 blanchet 2011-05-05 reverted 6efda6167e5d because unsound -- Vampire found a counterexample
2011-05-05 blanchet 2011-05-05 improve suggested type system list based on evaluation
2011-05-05 blanchet 2011-05-05 I have an intuition that it's sound to omit the first type arg of an hAPP -- and this reduces the size of monomorphized problems quite a bit
2011-05-05 blanchet 2011-05-05 removed unsound hAPP optimization
2011-05-05 blanchet 2011-05-05 versions of ! and ? for the ASCII-challenged Mirabelle
2011-05-05 blanchet 2011-05-05 smoother handling of ! and ? in type system names