src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
2011-05-22 blanchet 2011-05-22 improved Waldmeister support -- even run it by default on unit equational goals
2011-05-22 blanchet 2011-05-22 fish out axioms in Waldmeister output
2011-05-22 blanchet 2011-05-22 added support for remote Waldmeister
2011-05-20 blanchet 2011-05-20 name tuning
2011-05-20 blanchet 2011-05-20 further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
2011-05-20 blanchet 2011-05-20 prevent unsound combinator proofs in partially typed polymorphic type systems
2011-05-20 blanchet 2011-05-20 improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
2011-05-20 blanchet 2011-05-20 reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
2011-05-20 blanchet 2011-05-20 automatically use "metisFT" when typed helpers are necessary
2011-05-20 blanchet 2011-05-20 generate useful information for type axioms
2011-05-20 blanchet 2011-05-20 slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
2011-05-19 blanchet 2011-05-19 renamed "simple_types" to "simple"
2011-05-19 blanchet 2011-05-19 since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
2011-05-19 blanchet 2011-05-19 honor "conj_sym_kind" also for tag symbol declarations
2011-05-19 blanchet 2011-05-19 removed "poly_tags_light_bang" since highly unsound
2011-05-17 blanchet 2011-05-17 renamed thin to light, fat to heavy
2011-05-17 blanchet 2011-05-17 code cleanup, better handling of corner cases
2011-05-17 blanchet 2011-05-17 implemented thin versions of "preds" type systems + fixed various issues with type args
2011-05-17 blanchet 2011-05-17 renamed "shallow" to "thin" and make it the default
2011-05-17 blanchet 2011-05-17 more work on "shallow" encoding + adjustments to other encodings
2011-05-17 blanchet 2011-05-17 generate type classes predicates in new "shallow" encoding
2011-05-17 blanchet 2011-05-17 started implementing "shallow" type systems, based on ideas by Claessen et al.
2011-05-17 blanchet 2011-05-17 added syntax for "shallow" encodings
2011-05-13 blanchet 2011-05-13 optimized a common case
2011-05-13 blanchet 2011-05-13 avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed
2011-05-13 blanchet 2011-05-13 make SML/NJ happy
2011-05-12 blanchet 2011-05-12 fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
2011-05-12 blanchet 2011-05-12 robustly detect how many type args were passed to the ATP, even if some of them were omitted
2011-05-12 blanchet 2011-05-12 make sure "simple_types_query" and "simple_types_bang" symbols are declared with the proper types
2011-05-12 blanchet 2011-05-12 drop some type arguments to constants in unsound type systems + remove a few type systems that make no sense from the circulation
2011-05-12 blanchet 2011-05-12 ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded
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 unfold set constants in Sledgehammer/ATP as well if Metis does it too
2011-05-12 blanchet 2011-05-12 don't give weights to built-in symbols
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 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 renamed type systems for more consistency
2011-05-06 blanchet 2011-05-06 allow each prover to specify its own formula kind for symbols occurring in the conjecture
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 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 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 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
2011-05-04 blanchet 2011-05-04 tuning
2011-05-04 blanchet 2011-05-04 documentation tuning
2011-05-04 blanchet 2011-05-04 renamed "many_typed" to "simple" (as in simple types)
2011-05-04 blanchet 2011-05-04 added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
2011-05-04 blanchet 2011-05-04 exploit inferred monotonicity
2011-05-04 blanchet 2011-05-04 monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
2011-05-04 blanchet 2011-05-04 added type annotation for SML/NJ
2011-05-04 blanchet 2011-05-04 eta-expansion for SML/NJ
2011-05-03 blanchet 2011-05-03 cosmetics
2011-05-03 blanchet 2011-05-03 no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter