2010-07-27 blanchet 2010-07-27 complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
2010-07-27 blanchet 2010-07-27 renamed file
2010-07-27 blanchet 2010-07-27 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
2010-07-27 blanchet 2010-07-27 get rid of more dead wood
2010-07-27 blanchet 2010-07-27 implemented "sublinear" minimization algorithm
2010-07-27 blanchet 2010-07-27 extract sort constraints from FOFs properly; we can't rely on having them as separate literals anymore
2010-07-27 haftmann 2010-07-27 merged
2010-07-27 haftmann 2010-07-27 delete structure Basic_Record; avoid `record` in names in structure Record
2010-07-27 blanchet 2010-07-27 no polymorphic "var"
2010-07-27 blanchet 2010-07-27 merged
2010-07-27 blanchet 2010-07-27 shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
2010-07-27 blanchet 2010-07-27 negate tfree conjecture
2010-07-27 blanchet 2010-07-27 handle Vampire's equality proxy axiom correctly
2010-07-27 blanchet 2010-07-27 simplify code
2010-07-26 blanchet 2010-07-26 prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
2010-07-26 blanchet 2010-07-26 remove obsolete field in record
2010-07-26 blanchet 2010-07-26 simplify code
2010-07-26 blanchet 2010-07-26 get rid of obsolete "axiom ID" component, since it's now always 0
2010-07-26 blanchet 2010-07-26 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
2010-07-26 blanchet 2010-07-26 added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
2010-07-26 blanchet 2010-07-26 simplify code
2010-07-26 blanchet 2010-07-26 remove more Skolemization-aware code
2010-07-26 blanchet 2010-07-26 kill Skolem handling in Sledgehammer
2010-07-26 blanchet 2010-07-26 simplify "conjecture_shape" business, as a result of using FOF instead of CNF
2010-07-26 blanchet 2010-07-26 generate full first-order formulas (FOF) in Sledgehammer
2010-07-26 blanchet 2010-07-26 make TPTP generator accept full first-order formulas
2010-07-26 blanchet 2010-07-26 generate close formulas for SPASS, but not for the others (to avoid clutter)
2010-07-26 blanchet 2010-07-26 renamed internal function
2010-07-26 blanchet 2010-07-26 proof reconstruction for full FOF terms
2010-07-26 blanchet 2010-07-26 remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)
2010-07-26 blanchet 2010-07-26 reorder SPASS conjectures correctly, based on Flotter output
2010-07-27 paulson 2010-07-27 Deleted an obsolete file
2010-07-28 wenzelm 2010-07-28 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
2010-07-28 wenzelm 2010-07-28 use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
2010-07-27 wenzelm 2010-07-27 simplified handling of update_time -- do not store within deps;
2010-07-27 wenzelm 2010-07-27 clarified register_thy: clean slate via kill_thy, more precise CRITICAL section; tuned;
2010-07-27 wenzelm 2010-07-27 updated keywords;
2010-07-27 wenzelm 2010-07-27 updated manual concerning theory loader;
2010-07-27 wenzelm 2010-07-27 theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
2010-07-27 wenzelm 2010-07-27 avoid repeated File.read for theory text (as before); misc tuning and simplification;
2010-07-27 wenzelm 2010-07-27 tuned messages and comments;
2010-07-27 wenzelm 2010-07-27 simplified Thy_Header.read -- include Source.of_string_limited here; tuned;
2010-07-27 wenzelm 2010-07-27 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps; explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database; Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command; added Thy_Load.begin_theory for clarity; structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader; moved some basic commands from isar_cmd.ML to isar_syn.ML; misc tuning and simplification;
2010-07-27 wenzelm 2010-07-27 more precise stats;
2010-07-26 wenzelm 2010-07-26 merged
2010-07-26 haftmann 2010-07-26 quickcheck images of goals under registration morphisms
2010-07-26 haftmann 2010-07-26 get_registrations interface
2010-07-26 haftmann 2010-07-26 restored unusual snd-biased merge/join policy -- required due to non-conservative code setups
2010-07-26 haftmann 2010-07-26 merged
2010-07-26 haftmann 2010-07-26 reactivated Scala check
2010-07-26 haftmann 2010-07-26 corrected range check once more
2010-07-26 haftmann 2010-07-26 added Code_Natural.thy
2010-07-26 haftmann 2010-07-26 reactivated Scala check; tuned import order
2010-07-26 haftmann 2010-07-26 reactivated Scala check
2010-07-26 haftmann 2010-07-26 modified namespace policy
2010-07-26 haftmann 2010-07-26 use Natural as index type for Haskell and Scala
2010-07-25 blanchet 2010-07-25 merged
2010-07-23 blanchet 2010-07-23 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas.
2010-07-23 blanchet 2010-07-23 first step in using "fof" rather than "cnf" in TPTP problems
2010-07-23 blanchet 2010-07-23 fix polymorphic "val"