get rid of more dead wood

implemented "sublinear" minimization algorithm

extract sort constraints from FOFs properly; we can't rely on having them as separate literals anymore

merged

delete structure Basic_Record; avoid `record` in names in structure Record

no polymorphic "var"

merged

shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses

negate tfree conjecture

handle Vampire's equality proxy axiom correctly

simplify code

prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)

remove obsolete field in record

simplify code

get rid of obsolete "axiom ID" component, since it's now always 0

reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting

added extensionalization to Sledgehammer, mimicking what the Clausifier used to do

simplify code

remove more Skolemization-aware code

kill Skolem handling in Sledgehammer

simplify "conjecture_shape" business, as a result of using FOF instead of CNF

generate full first-order formulas (FOF) in Sledgehammer

make TPTP generator accept full first-order formulas

generate close formulas for SPASS, but not for the others (to avoid clutter)

renamed internal function

proof reconstruction for full FOF terms

remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)

reorder SPASS conjectures correctly, based on Flotter output

Deleted an obsolete file

explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;

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);

simplified handling of update_time -- do not store within deps;

clarified register_thy: clean slate via kill_thy, more precise CRITICAL section; tuned;

updated keywords;

updated manual concerning theory loader;

theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);

avoid repeated File.read for theory text (as before); misc tuning and simplification;

tuned messages and comments;

simplified Thy_Header.read -- include Source.of_string_limited here; tuned;

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;

more precise stats;

merged

quickcheck images of goals under registration morphisms

get_registrations interface

restored unusual snd-biased merge/join policy -- required due to non-conservative code setups

merged

reactivated Scala check

corrected range check once more

added Code_Natural.thy

reactivated Scala check; tuned import order

reactivated Scala check

modified namespace policy

use Natural as index type for Haskell and Scala

merged

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.

first step in using "fof" rather than "cnf" in TPTP problems

fix polymorphic "val"

temporarily deactivating check for Scala

another refinement chapter in the neverending numeral story

inductive_cases: crude parallelization via Par_List.map;