src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
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
2011-05-03 blanchet 2011-05-03 replaced some Unsynchronized.refs with Config.Ts
2011-05-02 blanchet 2011-05-02 do not declare TPTP built-ins, e.g. $true
2011-05-02 blanchet 2011-05-02 generate tags for simps, intros, and elims in TPTP poblems on demand
2011-05-02 blanchet 2011-05-02 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
2011-05-02 blanchet 2011-05-02 cosmetics
2011-05-02 blanchet 2011-05-02 make sure E type information constants are given a weight, even if they don't appear anywhere else
2011-05-01 blanchet 2011-05-01 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)
2011-05-01 blanchet 2011-05-01 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01 blanchet 2011-05-01 close formula universally, to make SPASS happy
2011-05-01 blanchet 2011-05-01 fixed embarrassing bug where conjecture and fact offsets were swapped
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-05-01 blanchet 2011-05-01 made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
2011-05-01 blanchet 2011-05-01 merge symbol declarations that are type-instances of each other -- useful for type system "Args true" with monomorphization turned off
2011-05-01 blanchet 2011-05-01 drop even more bound types in symbol declarations -- useful in particular for type system "Args true"
2011-05-01 blanchet 2011-05-01 tuning
2011-05-01 blanchet 2011-05-01 got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly
2011-05-01 blanchet 2011-05-01 drop "fequal" type args for unmangled type systems
2011-05-01 blanchet 2011-05-01 cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
2011-05-01 blanchet 2011-05-01 make sure that fequal keeps its type arguments for mangled type systems
2011-05-01 blanchet 2011-05-01 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
2011-05-01 blanchet 2011-05-01 avoid Type.TYPE_MATCH exception for "True_or_False" for "If"
2011-05-01 blanchet 2011-05-01 proper handling of partially applied proxy symbols
2011-05-01 blanchet 2011-05-01 make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type
2011-05-01 blanchet 2011-05-01 improve helper type instantiation code
2011-05-01 blanchet 2011-05-01 killed needless datatype "combtyp" in Metis
2011-05-01 blanchet 2011-05-01 have properly type-instantiated helper facts (combinators and If)
2011-05-01 blanchet 2011-05-01 don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set
2011-05-01 blanchet 2011-05-01 cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation
2011-05-01 blanchet 2011-05-01 fixed min-arity computation when "explicit_apply" is specified
2011-05-01 blanchet 2011-05-01 fixed "tags" type encoding after latest round of changes
2011-05-01 blanchet 2011-05-01 fix handling of proxies after recent drastic changes to the type encodings
2011-05-01 blanchet 2011-05-01 reconstruct TFF type predicates correctly for ToFoF
2011-05-01 blanchet 2011-05-01 handle special constants correctly in Isar proof reconstruction code, especially type predicates
2011-05-01 blanchet 2011-05-01 make sure the minimizer monomorphizes when it should
2011-05-01 blanchet 2011-05-01 fixed arity of special constants if "explicit_apply" is set
2011-05-01 blanchet 2011-05-01 make sure typing fact names are unique (needed e.g. by SNARK)
2011-05-01 blanchet 2011-05-01 minor cleanup
2011-05-01 blanchet 2011-05-01 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available