merged

tuned; added pretty numerals for code generation

may use `int` in Isabelle runtime environment

dropped dead code

merged

make Mirabelle happy

renamed environment variable

updated component name

consequence of directory renaming

rename directory

minor refactoring

minor refactoring

updated Sledgehammer docs

remove needless "-x" option, now that (1) we can't handle remote SPASS anymore; and (2) we can a priori parse the SPASS syntax in "Sledgehammer_Proof_Reconstruct" anyway

remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts

fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses

revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well; we can no longer just count the formulas, because for some reason E's numbering either no longer starts at 1 or it doesn't increment by 1 at each step

more robust proof reconstruction

adapt to new (?) TPTP output

fix remote_vampire's proof reconstruction

fix proof reconstruction for latest Vampire

renaming

support latest version of Vampire (1.0) locally

improve detection of installed SPASS

merged

merge

compile

minor refactoring

standardize "Author" tags

remove unused fun

reorder ML files in theory

get rid of "FOLClause" (obsoleted by FOF-enabled "FOLFormula")

more refactoring

kill needless tracing

rename "ATP_Manager" ML module to "Sledgehammer"; more refactoring to come

rename

complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"

renamed file

move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"

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;

modernized/unified some specifications;

Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;

simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants; eliminated obsolete touch_child_thys, register_theory;

simplified handling of theory begin/end wrt. toplevel and theory loader;

Thy_Load.check_loaded via Theory.at_end;

tuned;

moved basic thy file name operations from Thy_Load to Thy_Header;

moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;

merged

avoid unreliable Haskell Int type

proper subclass instead of sublocale

repaired tool invocation

observe standard conventions for doc-strings;

tuned message;

eliminated some unused Thy_Info operations;

refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;

generic external source files -- nothing special about ML here;

discontinued special treatment of ML files -- no longer complete extensions on demand; simplified Thy_Load.check_file, with uniform error reporting; added Thy_Load.test_file for non-strict checking; misc tuning and simplification;

eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL; reset_path is CRITICAL;

tuned signature;

updated some headers;