2010-06-25 ago blanchet move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
2010-06-28 ago wenzelm merged
2010-06-28 ago Cezary Kaliszyk Quotient package reverse lifting
2010-06-28 ago Cezary Kaliszyk Add reverse lifting flag to automated theorem derivation
2010-06-28 ago Cezary Kaliszyk Restrict quotient definitions to constants
2010-06-27 ago Christian Urban mixfix can be given for automatically lifted constants
2010-06-26 ago Christian Urban streamlined the generation of quotient theorems out of raw theorems
2010-06-25 ago haftmann merged
2010-06-25 ago haftmann avoid REPEAT after THEN_ALL_NEW
2010-06-26 ago wenzelm refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
2010-06-26 ago wenzelm treat alternative newline symbols as in Isabelle/ML;
2010-06-26 ago wenzelm simplified text_area_painter, with more precise treatment of visible line end;
2010-06-25 ago wenzelm merged
2010-06-25 ago blanchet merged
2010-06-25 ago blanchet eta-expand
2010-06-25 ago blanchet improve the natural formula relevance filter code, so that it behaves more like the CNF one
2010-06-25 ago blanchet split SPASS time slot between SOS and non-SOS, in case SOS times out
2010-06-24 ago blanchet yields ill-typed ATP/metis proofs -- raus!
2010-06-24 ago blanchet make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
2010-06-25 ago haftmann merged
2010-06-24 ago haftmann more direct definition simplifies proofs
2010-06-24 ago haftmann merged
2010-06-24 ago haftmann more precise tactic: do not escape to a different goal branch (REPEAT is still problematic, though)
2010-06-24 ago blanchet a76ace919f1c wasn't quite right; second try
2010-06-24 ago blanchet merge
2010-06-24 ago blanchet never include anything from the Sledgehammer theory in the relevant facts + killed two obsolete facts
2010-06-24 ago blanchet better eta-expansion in Sledgehammer's clausification;
2010-06-24 ago blanchet cosmetics
2010-06-24 ago blanchet make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
2010-06-23 ago blanchet improve the new "natural formula" fact filter
2010-06-25 ago wenzelm explicit treatment of UTF8 sequences as Isabelle symbols;
2010-06-24 ago wenzelm ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
2010-06-24 ago wenzelm escape UTF8 symbols for the ML compiler;
2010-06-24 ago wenzelm explicit treatment of UTF8 character sequences as Isabelle symbols;
2010-06-24 ago Christian Urban slight cleaning and simplification of the automatic wrapper for quotient definitions
2010-06-24 ago wenzelm merged
2010-06-24 ago Christian Urban export of proper information in the ML-interface of the quotient package
2010-06-24 ago wenzelm treat Pretty.T as strictly abstract type;
2010-06-24 ago wenzelm slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;
2010-06-24 ago wenzelm avoid equality on abstract type Pretty.T;
2010-06-24 ago wenzelm notes on packaging;
2010-06-24 ago wenzelm misc tuning;
2010-06-24 ago wenzelm tuned auxiliary structures;
2010-06-24 ago wenzelm Net.encode_type;
2010-06-24 ago wenzelm more accurate dependencies;
2010-06-24 ago haftmann made smlnj happy
2010-06-23 ago blanchet fix syntax bug in the TPTP output, by ensuring that "hBOOL" is correctly used for n-ary predicates even if (n + k)-ary occurrences of the same predicate, but with a different type, occur in the same problem
2010-06-23 ago blanchet renamed for easier grep
2010-06-23 ago blanchet use Skolem inlining also in the nonpolymorphic case, as a step toward simplifying the source code
2010-06-23 ago blanchet steal some of http://isabelle.in.tum.de/sledgehammer.html and add it to the docs
2010-06-23 ago blanchet have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
2010-06-23 ago blanchet fix bug with "skolem_id" + sort facts for increased readability
2010-06-23 ago blanchet if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
2010-06-23 ago blanchet merged
2010-06-23 ago blanchet this looks like the most appropriate place to do the beta-eta-contraction
2010-06-23 ago blanchet killed legacy "neg_clausify" and "clausify"
2010-06-22 ago blanchet merged
2010-06-22 ago blanchet factor out TPTP format output into file of its own, to facilitate further changes
2010-06-22 ago blanchet merged
2010-06-22 ago blanchet turn on "natural form" filtering in the Mirabelle tests, to see how it performs