src/HOL/Tools/ATP/atp_reconstruct.ML
2011-09-07 blanchet 2011-09-07 tuning
2011-09-07 blanchet 2011-09-07 perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
2011-08-22 blanchet 2011-08-22 added caching for (in)finiteness checks
2011-08-22 blanchet 2011-08-22 started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-07-28 blanchet 2011-07-28 put parentheses around non-trivial metis call
2011-07-20 blanchet 2011-07-20 pass type arguments to lambda-lifted Frees, to account for polymorphism
2011-07-17 blanchet 2011-07-17 ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
2011-07-05 nik 2011-07-05 improved translation of lambdas in THF
2011-06-20 blanchet 2011-06-20 clean up SPASS FLOTTER hack
2011-06-16 blanchet 2011-06-16 fixed soundness bug related to extensionality
2011-06-09 blanchet 2011-06-09 cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
2011-06-09 blanchet 2011-06-09 improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well
2011-06-08 blanchet 2011-06-08 avoid duplicate facts, which confuse the minimizer output
2011-06-08 blanchet 2011-06-08 don't generate unsound proof error for missing proofs
2011-06-07 blanchet 2011-06-07 use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
2011-06-07 blanchet 2011-06-07 obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-06 blanchet 2011-06-06 Metis code cleanup
2011-06-06 blanchet 2011-06-06 remove more occurrences of "metisX", preparing for the D Day when it will silently hijack "metis" and "metisFT"
2011-06-06 blanchet 2011-06-06 imported patch metis_reconstr_give_type_infer_a_chance
2011-06-06 blanchet 2011-06-06 make "metisX"'s default more like old "metis"
2011-06-06 blanchet 2011-06-06 fixed reconstruction of new Skolem constants in new Metis
2011-06-06 blanchet 2011-06-06 reveal Skolems in new Metis
2011-06-06 blanchet 2011-06-06 don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions
2011-06-06 blanchet 2011-06-06 slacker version of "fastype_of", in case a function has dummy type
2011-06-06 blanchet 2011-06-06 only uncombine combinators in textual Isar proofs, not in Metis
2011-06-06 blanchet 2011-06-06 temporarily added "MetisX" as reconstructor and minimizer
2011-06-06 blanchet 2011-06-06 show what failed to play
2011-06-06 blanchet 2011-06-06 killed odd connectives
2011-06-01 blanchet 2011-06-01 handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
2011-06-01 blanchet 2011-06-01 more uniform handling of tfree sort inference in ATP reconstruction code, based on what Metis always has done
2011-06-01 blanchet 2011-06-01 fixed interaction between type tags and hAPP in reconstruction code
2011-06-01 blanchet 2011-06-01 implemented missing hAPP and ti cases of new path finder
2011-06-01 blanchet 2011-06-01 export one more function
2011-05-31 blanchet 2011-05-31 tuned name
2011-05-31 blanchet 2011-05-31 more robust and simpler adjustment computation
2011-05-31 blanchet 2011-05-31 more work on new Metis
2011-05-31 blanchet 2011-05-31 tuning
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation